intro a_ne_z ab_eq_ac
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c : R
⊢ a ≠ 0 → a * b = a * c → b = c
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c : R
a_ne_z : a ≠ 0
ab_eq_ac : a * b = a * c
⊢ b = c