α : 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_lt_sdiff_iff_lt, sdiff_eq_empty_iff_subset.2 h.1]
no goals
α : Type u_1
inst✝ : LinearOrder α
A B : Finset α
h : A ⊂ B
⊢ toColex ∅ < toColex (B \ A)
exact empty_toColex_lt (by simpa [Finset.Nonempty] using exists_of_ssubset h)
no goals
α : Type u_1
inst✝ : LinearOrder α
A B : Finset α
h : A ⊂ B
⊢ Finset.Nonempty (B \ A)
simpa [Finset.Nonempty] using exists_of_ssubset h