no goals
M : Type u_2
N : Type ?u.62983
G : Type ?u.62986
A : Type u_1
B : Type ?u.62992
α : Type ?u.62995
β : Type ?u.62998
γ : Type ?u.63001
δ : Type ?u.63004
inst✝² : Monoid M
inst✝¹ : AddGroup A
inst✝ : DistribMulAction M A
r : M
x y : A
⊢ r • (x - y) = r • x - r • y
rw [sub_eq_add_neg, sub_eq_add_neg, smul_add, smul_neg]