R : Type u_1
V : Type u_2
V' : Type ?u.288204
P : Type u_3
P' : Type ?u.288210
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
w x y z : P
h₁ : Wbtw R w y z
h₂ : Sbtw R w x y
⊢ x ≠ z
R : Type u_1
V : Type u_2
V' : Type ?u.288204
P : Type u_3
P' : Type ?u.288210
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
w x y z : P
h₁ : Wbtw R w y z
h₂ : Sbtw R w x y
⊢ Sbtw R w x z
refine' ⟨h₁.trans_left h₂.wbtw, h₂.ne_left, _⟩
R : Type u_1
V : Type u_2
V' : Type ?u.288204
P : Type u_3
P' : Type ?u.288210
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
w x y : P
h₂ : Sbtw R w x y
h₁ : Wbtw R w y x
⊢ False
R : Type u_1
V : Type u_2
V' : Type ?u.288204
P : Type u_3
P' : Type ?u.288210
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
w x y z : P
h₁ : Wbtw R w y z
h₂ : Sbtw R w x y
⊢ x ≠ z
rintro rfl
no goals
R : Type u_1
V : Type u_2
V' : Type ?u.288204
P : Type u_3
P' : Type ?u.288210
inst✝⁷ : OrderedRing R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup V'
inst✝² : Module R V'
inst✝¹ : AddTorsor V' P'
inst✝ : NoZeroSMulDivisors R V
w x y : P
h₂ : Sbtw R w x y
h₁ : Wbtw R w y x
⊢ False
exact h₂.right_ne ((wbtw_swap_right_iff R w).1 ⟨h₁, h₂.wbtw⟩)