case h
α : Type u_1
inst✝ : CircularOrder α
a b x✝ : α
⊢ x✝ ∈ cIcc a bᶜ ↔ x✝ ∈ cIoo b a
α : Type u_1
inst✝ : CircularOrder α
a b : α
⊢ cIcc a bᶜ = cIoo b a
ext
case h
α : Type u_1
inst✝ : CircularOrder α
a b x✝ : α
⊢ x✝ ∈ cIcc a bᶜ ↔ ¬btw a x✝ b
case h
α : Type u_1
inst✝ : CircularOrder α
a b x✝ : α
⊢ x✝ ∈ cIcc a bᶜ ↔ x✝ ∈ cIoo b a
rw [Set.mem_cIoo, sbtw_iff_not_btw]
no goals
case h
α : Type u_1
inst✝ : CircularOrder α
a b x✝ : α
⊢ x✝ ∈ cIcc a bᶜ ↔ ¬btw a x✝ b
rfl