proposition: Lemma wH_bitstring n (x : 'rV_n) : wH x = HammingBitstring.wH (tval (rowF2_tuplebool x)).
proof: Proof. rewrite wH_num_occ /HammingBitstring.wH /= /num_occ /= [in RHS]count_map. apply eq_in_count => /= b Hb; by rewrite -(F2_eq1 b) eqb_id. 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