proposition: Lemma size_exp_monic (p: {poly R}) n : p \is monic -> size (p ^+ n) = ((size p).-1 * n).+1.
proof: Proof. move=> pM; elim: n => // [|n IH]. by rewrite !expr0 muln0 size_polyC oner_eq0. rewrite exprS size_proper_mul ?IH; last first. by rewrite (eqP pM) (eqP (monic_exp n pM)) mul1r oner_neq0. have : (0 < size p)%nat. by have := monic_neq0 pM; rewrite -size_poly_eq0; case: size. by case: size => // k _; rewrite addSn addnS -mulnS. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly)