no goals
R : Type u_1
inst✝⁴ : StrictOrderedCommRing R
M : Type u_2
N : Type ?u.144746
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)
rw [← sameRay_neg_iff, neg_neg]