proposition: Lemma size_factor (x : R) : size ('X + x%:P) = 2%N.
proof: Proof. by rewrite size_addl ?size_polyX // size_polyC /=; case: (x == 0). 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