. exact Nat.eq_of_mul_eq_mul_left zero_lt_a
case neg.mp
a b c : Nat
ha : ¬a = 0
zero_lt_a : 0 < a
⊢ a * b = a * c → b = c

case neg.mpr
a b c : Nat
ha : ¬a = 0
zero_lt_a : 0 < a
⊢ b = c → a * b = a * c
case neg.mpr
a b c : Nat
ha : ¬a = 0
zero_lt_a : 0 < a
⊢ b = c → a * b = a * c