proposition: Lemma wH_m_card n k : #|[set a in 'rV['F_2]_n | wH a == k]| = 'C(n, k).
proof: Proof. rewrite -[in X in _ = X](card_ord n) -card_draws -2!sum1dep_card. pose h' := fun s : {set 'I_n} => \row_(j < n) (if j \in s then (1 : 'F_2) else 0). have h'h (i : 'rV_n) : h' [set i0 | i ``_ i0 == 1] == i. apply/eqP/rowP => y; rewrite !mxE inE. case: ifP => [/eqP -> // | /negbT]; by rewrite -F2_eq0 => /eqP. rewrite (reindex_onto (fun x : 'rV_n => [set i | x ``_ i == 1]) h') /=. - apply eq_bigl => i. rewrite wH_num_occ num_occ_alt h'h andbC /=; congr (_ == _). apply eq_card => t; by rewrite !inE tnth_mktuple. - move=> s Hs. apply/setP => /= i; rewrite !inE /h' mxE; by case: ifP. Qed.
imports: Reals mathcomp(all_ssreflect fingroup zmodp ssralg finalg perm matrix) mathcomp(poly mxalgebra mxpoly) mathcomp(Rstruct) ssr_ext ssralg_ext f2 num_occ natbin ssrR Reals_ext bigop_ext