proposition: Lemma wH_poly_rV (p : {poly F}) : wH (poly_rV p) <= size p.
proof: Proof. rewrite /wH /=. case/boolP : (size p < n) => pn; last first. rewrite -leqNgt in pn; rewrite (leq_trans _ pn) //. by rewrite (leq_trans (count_size _ _)) // size_map size_enum_ord. have -> : [seq (poly_rV p) ``_ i | i <- enum 'I_n] = [seq (poly_rV p) ``_ i | i <- enum ('I_(size p))] ++ nseq (n - size p) 0. apply (@eq_from_nth _ 0) => [|i]. by rewrite size_cat 2!size_map !size_enum_ord size_nseq subnKC // ltnW. rewrite size_map size_enum_ord => ni. rewrite (nth_map (Ordinal ni)) ?size_enum_ord // mxE nth_enum_ord //. rewrite nth_cat size_map size_enum_ord; case: ifPn => [pi|]. by rewrite (nth_map (Ordinal pi)) ?size_enum_ord // mxE nth_enum_ord. rewrite -leqNgt => /leq_sizeP/(_ _ (leqnn i)) ->; by rewrite nth_nseq ltn_sub2r. rewrite count_cat [X in _ + X <= _](_ : count _ _ = O) ?addn0; last first. rewrite (@eq_in_count _ _ pred0) ?count_pred0 //. move=> i; case/nseqP => -> /= _; by rewrite eqxx. by rewrite count_map (leq_trans (count_size _ _)) // size_enum_ord. 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