no goals
α : Type u_1
β : Type ?u.47327
inst✝ : PartialOrder α
a b c : α
hab : a ≤ b
⊢ Ioc a b ∪ {a} = Icc a b
rw [← Icc_diff_left, diff_union_self,
  union_eq_self_of_subset_right (singleton_subset_iff.2 <| left_mem_Icc.2 hab)]