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 : R
h : Rel r a b
⊢ Rel r (-a) (-b)
simp only [neg_eq_neg_one_mul a, neg_eq_neg_one_mul b, Rel.mul_right h]