proposition: Lemma factor_complex_roots (z : C) : toC ('X^2 + (1 *- 2 * Re z) *: 'X + (Re z ^+ 2 + Im z ^+ 2)%:P) = ('X - z%:P) * ('X - (z^*)%:P).
proof: Proof. rewrite mulrBr !mulrBl opprB (addrC (z%:P * (z^*)%:P) _) addrA. rewrite (mulrC _ (z^*)%:P) -[in RHS](addrA ('X * 'X) _) -expr2. rewrite -(opprD (z%:P * 'X) ((z^*)%:P * 'X)). rewrite -(mulrDl z%:P _ 'X) -(polyCD z z^*) -(polyCM z z^*) -sqr_normc -re_conj normC_re_im mul_polyC -(opprK (Re z ^+ 2 + Im z ^+ 2)%:P) map_poly_is_additive -polyCN -mul_polyC map_polyC. rewrite -(opprK ((1 *- 2 * Re z)%:P * 'X)) map_poly_is_additive map_polyXn -(opprK (Re z ^+ 2 + Im z ^+ 2)%:C%:P) -(polyCN (Re z ^+ 2 + Im z ^+ 2)%:C). have H : (- (Re z ^+ 2 + Im z ^+ 2)%:C) = (- (Re z ^+ 2 + Im z ^+ 2))%:C. by rewrite -!complexr0 -{2}oppr0. rewrite H {H} -mulNr -(@polyCN _ (1 *- 2 * Re z)) mul_polyC map_polyZ map_polyX mulNr opprK. have H : 2%:R * (Re z)%:C = (2%:R * (Re z))%:C. rewrite -!complexr0. by simpc. 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)