no goals
R : Type u_1
V : Type u_2
V' : Type ?u.215069
P : Type u_3
P' : Type ?u.215075
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
x y z : P
h : Wbtw R x y z
⊢ Wbtw R y x z ↔ x = y
rw [← wbtw_swap_left_iff R z, and_iff_right h]