R : Type u₁
inst✝³ : Semiring R
S : Type u₂
inst✝² : CommSemiring S
A : Type u₃
inst✝¹ : Semiring A
inst✝ : Algebra S A
r : R → R → Prop
a b c : R
h : Rel r b c
⊢ Rel r (b + a) (c + a)
R : Type u₁
inst✝³ : Semiring R
S : Type u₂
inst✝² : CommSemiring S
A : Type u₃
inst✝¹ : Semiring A
inst✝ : Algebra S A
r : R → R → Prop
a b c : R
h : Rel r b c
⊢ Rel r (a + b) (a + c)
rw [add_comm a b, add_comm a c]
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 : R → R → Prop
a b c : R
h : Rel r b c
⊢ Rel r (b + a) (c + a)
exact Rel.add_left h