proposition: Lemma root_shift_2 (p : {poly R}) (a x : R) : root p (x + a) = root (p \shift a) x.
proof: Proof. by rewrite !rootE -{2}(@addrK _ a x) -horner_shift_poly1. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex) poly_normal pol