proposition: Lemma cardinal_tuple_nm n m: #|[set s: m.-tuple bool | DP_Tcount s == n]| = 'C(m,n).
proof: Proof. move: (card_draws 'I_m n); rewrite card_ord => <-. rewrite card_set_pred -(card_imset _ (@list_to_set_inj m));apply: eq_card => x. rewrite !inE; apply/imsetP/idP => [ [y yp yv] | cx]. by rewrite set_to_list_cardinal yv (list_to_setK (size_tuple y))//. have sm: size (char_seq x) == m by rewrite size_char_seq. set y:= Tuple sm. move:(list_to_setK (size_tuple y)) (set_to_listK x) => tt w. by exists y => //; rewrite inE - tt -set_to_list_cardinal w. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)