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