proposition: Lemma scaleX_poly_is_linear (c : R) : linear (scaleX_poly c).
proof: Proof. by move=> a u v; rewrite /scaleX_poly comp_polyD comp_polyZ. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex) poly_normal pol