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 : A → A → Prop
k : S
a b : A
h : Rel r a b
⊢ Rel r (k • a) (k • b)
simp only [Algebra.smul_def, Rel.mul_right h]