proposition: Lemma size_factor_expr : forall (t : R)(n : nat), size (('X + t%:P)^+n) = n.+1.
proof: Proof. move=> t; elim=> [|n ihn]; first by rewrite expr0 size_polyC oner_eq0. rewrite exprS size_monicM //; last first. by rewrite -size_poly_eq0 ihn; apply/negP; move/eqP. by rewrite -(opprK t%:P) -polyCN monicXsubC. by rewrite ihn -(opprK t%:P) -polyCN size_XsubC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat binomial seq choice order) mathcomp(fintype bigop ssralg poly ssrnum ssrint rat ssrnum) mathcomp(polyrcf qe_rcf_th realalg) pol poly_normal desc