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
hv : v ≠ 0
r : R
hr : r ≠ 0
⊢ SameRay R v (r • v) ↔ 0 < r
simp only [sameRay_smul_right_iff, hv, or_false_iff, hr.symm.le_iff_lt]