no goals
ι : Type ?u.119351
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderBot α
b : α
⊢ Iic b = cons b (Iio b) (_ : ¬b ∈ Iio b)
classical rw [cons_eq_insert, Iio_insert]
no goals
ι : Type ?u.119351
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderBot α
b : α
⊢ Iic b = cons b (Iio b) (_ : ¬b ∈ Iio b)
rw [cons_eq_insert, Iio_insert]