no goals
R : Type u_1
inst✝⁴ : StrictOrderedCommRing R
M : Type u_2
N : Type ?u.141134
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M
⊢ SameRay R (-x) (-y) ↔ SameRay R x y
simp only [SameRay, neg_eq_zero, smul_neg, neg_inj]