Theorem: Misc.Nat.lt_of_mul_lt_mul_left (LeanSAT/Util/Misc.lean)

State before:
a b c : Nat
h : a * b < a * c
a0 : 0 < a
⊢ b < c
Tactic:
rw [← Nat.mul_lt_mul_left a0]
State after:
a b c : Nat
h : a * b < a * c
a0 : 0 < a
⊢ a * b < a * c

State before:
a b c : Nat
h : a * b < a * c
a0 : 0 < a
⊢ a * b < a * c
Tactic:
exact h
State after:
no goals