α : Type ?u.14071
β : Type ?u.14074
inst✝ : LinearOrder α
s : Finset α
h : Finset.Nonempty s
⊢ 0 < card s
α : Type ?u.14071
β : Type ?u.14074
inst✝ : LinearOrder α
s : Finset α
h : Finset.Nonempty s
⊢ 0 < List.length (sort (fun x x_1 => x ≤ x_1) s)
rw [length_sort]
no goals
α : Type ?u.14071
β : Type ?u.14074
inst✝ : LinearOrder α
s : Finset α
h : Finset.Nonempty s
⊢ 0 < card s
exact card_pos.2 h