no goals
ι : Type ?u.115956
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ Ici a = cons a (Ioi a) (_ : ¬a ∈ Ioi a)
classical rw [cons_eq_insert, Ioi_insert]
no goals
ι : Type ?u.115956
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ Ici a = cons a (Ioi a) (_ : ¬a ∈ Ioi a)
rw [cons_eq_insert, Ioi_insert]