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