α : Type u_1
inst✝ : LinearOrder α
A B : Finset α
h : A ⊆ B
⊢ toColex ∅ ≤ toColex (B \ A)
α : Type u_1
inst✝ : LinearOrder α
A B : Finset α
h : A ⊆ B
⊢ toColex A ≤ toColex B
rw [← sdiff_le_sdiff_iff_le, sdiff_eq_empty_iff_subset.2 h]
no goals
α : Type u_1
inst✝ : LinearOrder α
A B : Finset α
h : A ⊆ B
⊢ toColex ∅ ≤ toColex (B \ A)
apply empty_toColex_le