proposition: Lemma scaleX_poly_multiplicative (c : R) : multiplicative (scaleX_poly c).
proof: Proof. split. move=> x y; exact: comp_polyM. by rewrite /scaleX_poly comp_polyC. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex) poly_normal pol