R : Type u_1
V : Type u_2
V' : Type ?u.578788
P : Type u_3
P' : Type ?u.578794
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w x y z : P
h₁ : Wbtw R z x w
h₂ : Wbtw R z y x
⊢ Wbtw R y x w
R : Type u_1
V : Type u_2
V' : Type ?u.578788
P : Type u_3
P' : Type ?u.578794
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w x y z : P
h₁ : Wbtw R w x z
h₂ : Wbtw R x y z
⊢ Wbtw R w x y
rw [wbtw_comm] at *
no goals
R : Type u_1
V : Type u_2
V' : Type ?u.578788
P : Type u_3
P' : Type ?u.578794
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w x y z : P
h₁ : Wbtw R z x w
h₂ : Wbtw R z y x
⊢ Wbtw R y x w
exact h₁.trans_left_right h₂