proposition: Lemma wH_count n (x : 'rV['F_2]_n) : wH x = count (fun i => x ``_ i == 1) (enum 'I_n).
proof: Proof. rewrite wH_sum -sum1_count [in RHS]big_mkcond /=. apply congr_big => //. - by rewrite /index_enum -enumT. - move=> i _; case: ifPn => [/eqP -> //|]. by rewrite -F2_eq0 => /eqP ->. 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