proposition: Lemma ex_subset_card B k : k <= #{B} -> exists2 A : {set T}, A \subset B & #{A} == k.
proof: Proof. Proof using. rewrite -bin_gt0 -(cards_draws B k) card_gt0 => /set0Pn [x]. by rewrite inE => /andP[H1 H2]; exists x. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype