no goals
ι : Type ?u.108656
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h : a < b
⊢ Ioc a b = cons b (Ioo a b) (_ : ¬b ∈ Ioo a b)
classical rw [cons_eq_insert, Ioo_insert_right h]
no goals
ι : Type ?u.108656
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h : a < b
⊢ Ioc a b = cons b (Ioo a b) (_ : ¬b ∈ Ioo a b)
rw [cons_eq_insert, Ioo_insert_right h]