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