α : Type u_1
β : Type ?u.44269
inst✝ : PartialOrder α
a b c : α
h : a ≤ b
⊢ {a, b} ⊆ Icc a b
α : Type u_1
β : Type ?u.44269
inst✝ : PartialOrder α
a b c : α
h : a ≤ b
⊢ Icc a b \ Ioo a b = {a, b}
rw [← Icc_diff_both, diff_diff_cancel_left]
no goals
α : Type u_1
β : Type ?u.44269
inst✝ : PartialOrder α
a b c : α
h : a ≤ b
⊢ {a, b} ⊆ Icc a b
simp [insert_subset, h]