R : Type u_1
inst✝⁶ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type ?u.7004
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type ?u.7086
inst✝¹ : DecidableEq ι
x✝ y z x : M
inst✝ : Nontrivial R
⊢ SameRay R x x
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type ?u.7004
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type ?u.7086
inst✝ : DecidableEq ι
x✝ y z x : M
⊢ SameRay R x x
nontriviality R
no goals
R : Type u_1
inst✝⁶ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type ?u.7004
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type ?u.7086
inst✝¹ : DecidableEq ι
x✝ y z x : M
inst✝ : Nontrivial R
⊢ SameRay R x x
exact Or.inr (Or.inr <| ⟨1, 1, zero_lt_one, zero_lt_one, rfl⟩)