no goals
R : Type u_2
inst✝³ : LinearOrderedCommRing R
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
v : M
r : R
hv : v ≠ 0
hr : r ≠ 0
⊢ SameRay R (-v) (r • v) ↔ r < 0
simp only [sameRay_neg_smul_right_iff, hv, or_false_iff, hr.le_iff_lt]