proposition: Lemma root_reciprocal_2 (p : {poly R}) (x : R) : x != 0 -> root p (x^-1) = root (reciprocal_pol p) x.
proof: Proof. move=> Hx. rewrite !rootE horner_reciprocal ?unitfE//. by rewrite mulrI_eq0 //; apply/lregX/lregP. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex) poly_normal pol