proposition: Lemma cards_draws T (B : {set T}) k : #|[set A : {set T} | A \subset B & #|A| == k]| = 'C(#|B|, k).
proof: Proof. have [ltTk | lekT] := ltnP #|B| k. rewrite bin_small // eq_card0 // => A. rewrite inE eqn_leq [k <= _]leqNgt. have [AsubB /=|//] := boolP (A \subset B). by rewrite (leq_ltn_trans (subset_leq_card AsubB)) ?andbF. apply/eqP; rewrite -(eqn_pmul2r (fact_gt0 k)) bin_ffact // eq_sym. rewrite -sum_nat_cond_const -{1 3}(card_ord k). rewrite -card_inj_ffuns_on -sum1dep_card. pose imIk (f : {ffun 'I_k -> T}) := f @: 'I_k. rewrite (partition_big imIk (fun A => (A \subset B) && (#|A| == k))) /= => [|f]; last first. move=> /andP [/ffun_onP f_ffun /injectiveP inj_f]. rewrite card_imset ?card_ord // eqxx andbT. by apply/subsetP => x /imsetP [i _ ->]; rewrite f_ffun. apply/eqP; apply: eq_bigr => A /andP [AsubB /eqP cardAk]. have [f0 inj_f0 im_f0]: exists2 f, injective f & f @: 'I_k = A. rewrite -cardAk; exists enum_val; first exact: enum_val_inj. apply/setP=> a; apply/imsetP/idP=> [[i _ ->] | Aa]; first exact: enum_valP. by exists (enum_rank_in Aa a); rewrite ?enum_rankK_in. rewrite (reindex (fun p : {ffun _} => [ffun i => f0 (p i)])) /=; last first. pose ff0' f i := odflt i [pick j | f i == f0 j]. exists (fun f => [ffun i => ff0' f i]) => [p _ | f]. apply/ffunP=> i; rewrite ffunE /ff0'; case: pickP => [j | /(_ (p i))]. by rewrite ffunE (inj_eq inj_f0) => /eqP. by rewrite ffunE eqxx. rewrite -im_f0 => /andP[/andP[/ffun_onP f_ffun /injectiveP injf] /eqP im_f]. apply/ffunP=> i; rewrite !ffunE /ff0'; case: pickP => [y /eqP //|]. have /imsetP[j _ eq_f0j_fi]: f i \in f0 @: 'I_k by rewrite -im_f imset_f. by move/(_ j)/eqP. rewrite -ffactnn -card_inj_ffuns -sum1dep_card; apply: eq_bigl => p. rewrite -andbA. apply/and3P/injectiveP=> [[_ /injectiveP inj_f0p _] i j eq_pij | inj_p]. by apply: inj_f0p; rewrite !ffunE eq_pij. set f := finfun _. have injf: injective f by move=> i j /[!ffunE] /inj_f0; apply: inj_p. have imIkf : imIk f == A. rewrite eqEcard card_imset // cardAk card_ord leqnn andbT -im_f0. by apply/subsetP=> x /imsetP[i _ ->]; rewrite ffunE imset_f. split; [|exact/injectiveP|exact: imIkf]. by apply/ffun_onP => x; apply: (subsetP AsubB); rewrite -(eqP imIkf) imset_f. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div fintype tuple finfun bigop prime finset)