no goals
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b : α
h : pred a < b
⊢ Ico (pred a) b = insert (pred a) (Ico a b)
simp_rw [← Ici_inter_Iio, Ici_pred, insert_inter_of_mem (mem_Iio.2 h)]