theorem Set.Nonempty.card_pos {α : Type u_1} {s : Set α} (hs : s.Nonempty) (hs' : s.Finite) : 0 < Nat.card ↑s