no goals
α : Type ?u.102675
R : Type u_2
k : Type ?u.102681
S : Type ?u.102684
M : Type u_1
M₂ : Type ?u.102690
M₃ : Type ?u.102693
ι : Type ?u.102696
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r s : R
x y : M
⊢ -r • -x = r • x
rw [neg_smul, smul_neg, neg_neg]