proposition: Lemma size_polyX_mul (p : {poly R}) : size ('X * p) = if p == 0 then 0%nat else (size p).+1.
proof: Proof. rewrite (_ : 'X * p = p * 'X + 0%:P); last by rewrite mulrC addr0. by rewrite size_MXaddC eqxx andbT. 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