proposition: Lemma complex_root_div_poly_deg2 : forall (p : {poly R}) (z : C), ((Im z) != 0) -> root (toC p) z -> ('X^2 + (- 2%:R * (Re z)) *: 'X + ((Re z) ^+2 + (Im z)^+2)%:P) %| p.
proof: Proof. move=> p z Hz Hrootz. have Hrootzbar : root (toC p) z^*. by rewrite -complex_root_conj_polyR. have Hp := (factor_complex_roots z). rewrite -(dvdp_map ((ComplexField.real_complex_rmorphism R))) /= Hp. rewrite Gauss_dvdp. apply/andP; split; by rewrite -root_factor_theorem. apply: Pdiv.ClosedField.root_coprimep => x. rewrite root_XsubC =>/eqP ->. clear x. rewrite hornerXsubC im_conj eq_complex ReiNIm ImiRe /= !addr0 !mulr0 subr0 add0r mul0r oppr0. rewrite eqxx mulrI_eq0 ?negb_and. apply/orP; by right. apply/lregP. by rewrite paddr_eq0 ?ler01 // negb_and oner_neq0. 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)