proposition: Lemma wH_3 : forall n, (3 <= n)%N -> wH (rV_of_nat n 3) = 2%N.
proof: Proof. case => // [] // [] // [] // n _. rewrite /wH /num_occ /rV_of_nat. set tmp := tuple_of_row _. have -> : tmp = [tuple of rev (1 :: 1 :: nseq n.+1 0)]%R. apply eq_from_tnth => i. rewrite tnth_mktuple mxE. rewrite -(nth_map _ 0%R); last by rewrite size_cat size_nseq /= addn2. rewrite (tnth_nth 0%R); congr ( _ `_ i)%R. rewrite /= (_ : 0 :: nseq n 0 = nseq n.+1 0)%R //. rewrite nseq_S -[in RHS]cat1s -[in RHS](cat1s _ (rcons _ _)) catA rev_cat. rewrite [in RHS]rev_rcons /=; congr (_ :: _). by rewrite rev_nseq map_cat map_nseq. rewrite /=. set y := _ :: _. rewrite (_ : y = [:: 1; 1; 0] ++ nseq n 0)%R // rev_cat count_cat /= -(@eq_in_count _ pred0). by rewrite count_pred0. move=> /= b; by 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