proposition: Lemma size_exp p n : (size (p ^+ n)).-1 = ((size p).-1 * n)%N.
proof: Proof. elim: n => [|n IHn]; first by rewrite size_poly1 muln0. have [-> | nz_p] := eqVneq p 0; first by rewrite exprS mul0r size_poly0. rewrite exprS size_mul ?expf_neq0 // mulnS -{}IHn. by rewrite polySpred // [size (p ^+ n)]polySpred ?expf_neq0 ?addnS. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)