proposition: Lemma wH_two_pow n p : p < n -> wH (rV_of_nat n (expn 2 p)) = 1%nat.
proof: Proof. move=> pn. rewrite wH_bitstring /rV_of_nat /row_of_bitseq /row_of_seq /rowF2_tuplebool /=. rewrite /HammingBitstring.wH /num_occ count_map. rewrite (eq_count (a2 := pred1 1)); last by move=> ? /=; rewrite eqb_id F2_eq1. rewrite -sum1_count big_map /=. rewrite (eq_bigl (pred1 (Ordinal (rev_ord_proof (Ordinal pn))))); last first. move=> i /=; symmetry; rewrite -[in X in X = _]val_eqE /=. rewrite mxE bitseq_of_nat_expn2 // nth_cat size_nseq. case: ifP => [ i_m | /negbT ]. rewrite nth_nseq i_m /=. apply/negbTE; by rewrite neq_ltn i_m. rewrite -leqNgt leq_eqVlt; case/orP => [/eqP Heq | npi]. by rewrite -Heq subnn /= !eqxx. rewrite -[in X in _ = X]subnSK //= nth_nseq. transitivity false; last by case: ifP. apply/negbTE; by rewrite neq_ltn npi orbC. by rewrite /= big_filter_cond /= big_pred1_eq. 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