. simp only [ha, Nat.zero_mul, or_true]
case pos
a b c : Nat
ha : a = 0
⊢ a * b = a * c ↔ b = c ∨ a = 0

case neg
a b c : Nat
ha : ¬a = 0
⊢ a * b = a * c ↔ b = c ∨ a = 0
case neg
a b c : Nat
ha : ¬a = 0
⊢ a * b = a * c ↔ b = c ∨ a = 0