no goals
α : Type ?u.98570
R : Type u_2
k : Type ?u.98576
S : Type ?u.98579
M : Type u_1
M₂ : Type ?u.98585
M₃ : Type ?u.98588
ι : Type ?u.98591
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r s : R
x y : M
⊢ -r • x + r • x = 0
rw [← add_smul, add_left_neg, zero_smul]