proposition: Lemma scaleX_polyC (c a : R) : a%:P \scale c = a%:P.
proof: Proof. 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