constructor
case neg
a c b : Nat
hc : ¬c = 0
zero_lt_c : 0 < c
⊢ a * c = b * c ↔ a = b
case neg.mp
a c b : Nat
hc : ¬c = 0
zero_lt_c : 0 < c
⊢ a * c = b * c → a = b

case neg.mpr
a c b : Nat
hc : ¬c = 0
zero_lt_c : 0 < c
⊢ a = b → a * c = b * c