. simp only [ha, or_false]
  have zero_lt_a : 0 < a := Nat.zero_lt_of_ne_zero ha
  constructor
  . exact Nat.eq_of_mul_eq_mul_left zero_lt_a
  . intro h
    rw [h]
case neg
a b c : Nat
ha : ¬a = 0
⊢ a * b = a * c ↔ b = c ∨ a = 0
no goals