proposition: Lemma wH_7 : forall n, (3 <= n)%N -> wH (rV_of_nat n 7) = 3%N.
proof: Proof. case => // [] // [] // [] // n _. rewrite /wH /num_occ /rV_of_nat. set x := tuple_of_row _. have -> : x =[tuple of rev (1 :: 1 :: 1 :: nseq n 0)]%R. rewrite /x {x}. apply eq_from_tnth => i. rewrite tnth_mktuple mxE (tnth_nth 0%R). rewrite -(nth_map _ ord0); last first. rewrite /pad_seqL /=. destruct n => //=. by rewrite size_cat size_nseq /= addn3. congr (_ `_ i)%R. rewrite /bitseq_of_nat /= !rev_cons /= /pad_seqL /= -addn3 addnK map_cat /= map_nseq /=. by rewrite rev_nseq -!cats1 /= -!catA. rewrite /=. set y := _ :: _. rewrite (_ : y = [:: 1; 1; 1] ++ nseq n 0)%R // rev_cat count_cat /=. rewrite -(@eq_in_count _ pred0) ?count_pred0 //. by move=> /= b; rewrite rev_nseq => /nseqP[->]. 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