case h
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type ?u.180935
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x✝ y : M
inst✝ : NoZeroSMulDivisors R M
x : M
hx : x ≠ 0
⊢ rayOfNeZero R x hx ≠ -rayOfNeZero R x hx
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type ?u.180935
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x✝ y : M
inst✝ : NoZeroSMulDivisors R M
x : Ray R M
⊢ x ≠ -x
induction' x using Module.Ray.ind with x hx
case h
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type ?u.180935
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x✝ y : M
inst✝ : NoZeroSMulDivisors R M
x : M
hx : x ≠ 0
⊢ ¬SameRay R x (-x)
case h
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type ?u.180935
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x✝ y : M
inst✝ : NoZeroSMulDivisors R M
x : M
hx : x ≠ 0
⊢ rayOfNeZero R x hx ≠ -rayOfNeZero R x hx
rw [neg_rayOfNeZero, Ne.def, ray_eq_iff]
no goals
case h
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type ?u.180935
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x✝ y : M
inst✝ : NoZeroSMulDivisors R M
x : M
hx : x ≠ 0
⊢ ¬SameRay R x (-x)
exact mt eq_zero_of_sameRay_self_neg hx