no goals
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b : α
h : pred a ≤ b
⊢ Icc (pred a) b = insert (pred a) (Icc a b)
simp_rw [← Ici_inter_Iic, Ici_pred, insert_inter_of_mem (mem_Iic.2 h)]