proposition: Lemma wH_7_rev7 n : (2 < n)%N -> wH (rV_of_nat n 7) = wH (rV_of_nat n (7 * expn 2 (n - 3))).
proof: Proof. move=> Hn. rewrite 2!wH_num_occ /rV_of_nat. set lhs := tuple_of_row _. set rhs := tuple_of_row _. suff <- : rev lhs = rhs by apply num_occ_rev. rewrite /lhs /rhs. rewrite /row_of_bitseq. rewrite -!row_of_seqK. rewrite -map_rev. by rewrite rev_bitseq_of_nat_7. 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