no goals
R✝ : Type u₁
inst✝⁴ : Semiring R✝
S : Type u₂
inst✝³ : CommSemiring S
A : Type u₃
inst✝² : Semiring A
inst✝¹ : Algebra S A
R : Type u₁
inst✝ : Ring R
r : R → R → Prop
a b c : R
h : Rel r b c
⊢ Rel r (a - b) (a - c)
simp only [sub_eq_add_neg, h.neg.add_right]