constructor
case neg
a b c : Nat
ha : ¬a = 0
zero_lt_a : 0 < a
⊢ a * b = a * c ↔ b = c
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