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