proposition: Lemma real_root_div_poly_deg1 (p : {poly R}) (z : C) : Im z = 0 -> root (toC p) z -> ('X - (Re z)%:P) %| p.
proof: Proof. move=>Himz Hroot. rewrite root_factor_theorem (@complexE _ z) Himz mulr0 addr0 in Hroot. rewrite -(dvdp_map ((ComplexField.real_complex_rmorphism R))) /=. have H : toC ('X - (Re z)%:P) = 'X - ((Re z)%:C)%:P. by rewrite map_poly_is_additive map_polyC map_polyX. by rewrite H. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path choice fintype order) mathcomp(prime div bigop ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex)