no goals
R : Type u_1
V : Type ?u.263675
V' : Type ?u.263678
P : Type ?u.263681
P' : Type ?u.263684
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'
x : R
⊢ Wbtw R 1 x 0 ↔ x ∈ Set.Icc 0 1
rw [wbtw_comm, wbtw_zero_one_iff]