proposition: Lemma card_draws T k : #|[set A : {set T} | #|A| == k]| = 'C(#|T|, k).
proof: Proof. by rewrite -cardsT -cards_draws; apply: eq_card => A; rewrite !inE subsetT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div fintype tuple finfun bigop prime finset)