no goals
α : Type ?u.23141
β : Type ?u.23144
inst✝ : LinearOrder α
s : Finset α
h : Finset.Nonempty s
⊢ List.length (sort (fun x x_1 => x ≤ x_1) s) - 1 < List.length (sort (fun x x_1 => x ≤ x_1) s)
simpa using Nat.sub_lt (card_pos.mpr h) zero_lt_one