no goals
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : PredOrder α
a b : α
inst✝ : NoMinOrder α
h : a < b
⊢ Ioo (pred a) b = insert a (Ioo a b)
simp_rw [← Ioi_inter_Iio, Ioi_pred_eq_insert, insert_inter_of_mem (mem_Iio.2 h)]