proposition: Lemma size_amul_expr : forall (t c : R)(i : nat), c != 0 -> size (('X * c%:P + t%:P) ^+ i) = i.+1.
proof: Proof. move=> t c; elim=> [| i ih] cn0; first by rewrite expr0 size_poly1. have hn0 : size ('X * c%:P + t%:P) = 2%N. rewrite mulrC size_MXaddC polyC_eq0. move: cn0; rewrite -eqbF_neg=> /eqP => cn0. by rewrite size_polyC cn0 andFb. by rewrite exprS size_mul // ?expf_eq0 -?size_poly_eq0 hn0 ?andbF // ih. 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