R : Type u_1
V : Type ?u.266529
V' : Type ?u.266532
P : Type ?u.266535
P' : Type ?u.266538
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
⊢ (0 ≤ x ∧ x ≤ 1) ∧ x ≠ 0 ∧ x ≠ 1 ↔ 0 < x ∧ x < 1
R : Type u_1
V : Type ?u.266529
V' : Type ?u.266532
P : Type ?u.266535
P' : Type ?u.266538
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
⊢ Sbtw R 0 x 1 ↔ x ∈ Set.Ioo 0 1
rw [Sbtw, wbtw_zero_one_iff, Set.mem_Icc, Set.mem_Ioo]
no goals
R : Type u_1
V : Type ?u.266529
V' : Type ?u.266532
P : Type ?u.266535
P' : Type ?u.266538
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
⊢ (0 ≤ x ∧ x ≤ 1) ∧ x ≠ 0 ∧ x ≠ 1 ↔ 0 < x ∧ x < 1
exact
  ⟨fun h => ⟨h.1.1.lt_of_ne (Ne.symm h.2.1), h.1.2.lt_of_ne h.2.2⟩, fun h =>
    ⟨⟨h.1.le, h.2.le⟩, h.1.ne', h.2.ne⟩⟩