ext x
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
⊢ Ioc a b = Ioc a c \ Ioc b c
case a
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidableEq α
hb : b ∈ Icc a c
x : α
⊢ x ∈ Ioc a b ↔ x ∈ Ioc a c \ Ioc b c