proposition: Lemma size_scaleX c p : c != 0 -> size (p \scale c) = size p.
proof: Proof. by move=> cu; rewrite size_comp_poly2 // size_XmulC. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)