R : Type u_1
V : Type u_2
V' : Type ?u.292206
P : Type u_3
P' : Type ?u.292212
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 z x w
h₂ : Sbtw R x y z
⊢ Sbtw R w y z
R : Type u_1
V : Type u_2
V' : Type ?u.292206
P : Type u_3
P' : Type ?u.292212
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 x z
h₂ : Sbtw R x y z
⊢ Sbtw R w y z
rw [wbtw_comm] at *
R : Type u_1
V : Type u_2
V' : Type ?u.292206
P : Type u_3
P' : Type ?u.292212
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 z x w
h₂ : Sbtw R z y x
⊢ Sbtw R z y w
R : Type u_1
V : Type u_2
V' : Type ?u.292206
P : Type u_3
P' : Type ?u.292212
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 z x w
h₂ : Sbtw R x y z
⊢ Sbtw R w y z
rw [sbtw_comm] at *
no goals
R : Type u_1
V : Type u_2
V' : Type ?u.292206
P : Type u_3
P' : Type ?u.292212
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 z x w
h₂ : Sbtw R z y x
⊢ Sbtw R z y w
exact h₁.trans_sbtw_left h₂