rw [←add_left_inj (-c), add_neg_self c]
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c : R
a_ne_z : a ≠ 0
ab_eq_ac : a * (b + -c) = 0
h : b + -c = 0
⊢ b = c
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c : R
a_ne_z : a ≠ 0
ab_eq_ac : a * (b + -c) = 0
h : b + -c = 0
⊢ b + -c = 0