proposition: Lemma root_scale_2 (p : {poly R}) (a x : R) : root p (a * x) = root (p \scale a) x.
proof: Proof. by rewrite !rootE horner_scaleX_poly. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex) poly_normal pol