no goals
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : PredOrder α
a b : α
inst✝ : NoMinOrder α
h : a ≤ b
⊢ Ioc (pred a) b = insert a (Ioc a b)
simp_rw [← Ioi_inter_Iic, Ioi_pred_eq_insert, insert_inter_of_mem (mem_Iic.2 h)]