no goals
M : Type u_2
N : Type ?u.62017
G : Type ?u.62020
A : Type u_1
B : Type ?u.62026
α : Type ?u.62029
β : Type ?u.62032
γ : Type ?u.62035
δ : Type ?u.62038
inst✝² : Monoid M
inst✝¹ : AddGroup A
inst✝ : DistribMulAction M A
r : M
x : A
⊢ r • -x + r • x = 0
rw [← smul_add, neg_add_self, smul_zero]