proposition: Lemma size_exp_leq p n : size (p ^+ n) <= ((size p).-1 * n).+1.
proof: Proof. elim: n => [|n IHn]; first by rewrite size_poly1. have [-> | nzp] := poly0Vpos p; first by rewrite exprS mul0r size_poly0. rewrite exprS (leq_trans (size_mul_leq _ _)) //. by rewrite -{1}(prednK nzp) mulnS -addnS leq_add2l. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)