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

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