proposition: Lemma quad_monic_normal (z : C) : (('X^2 + (- 2%:R * Re z) *: 'X + (Re z ^+2 + Im z ^+2)%:P) \is normal) = inB z.
proof: Proof. rewrite normalE -(mulr1 'X^2) mulrC mul_polyC polyseq_deg2 ?oner_neq0 //=. rewrite /inB -(@nmulr_rge0 _ (- 2%:R)) -?oppr_gt0 ?opprK ?ltr0Sn // ltr01 andbT. apply: andb_id2l => Hrez. rewrite mulr1. rewrite exprMn_comm; last first. rewrite /GRing.comm. by rewrite -mulNrn mulrC. rewrite sqrrN. rewrite -natrX. rewrite mulr_natl. rewrite [_ ^+2 *+ _]mulrS ler_add2l -mulr_natl -andbA /=. apply/idP/idP => [/orP [] | H]. rewrite eq_sym paddr_eq0 ?sqr_ge0 //. case/andP => /eqP -> /eqP ->. by rewrite mulr0. by case/andP. rewrite le_eqVlt in Hrez. case/orP : Hrez => [ | Hrez]. rewrite eq_sym mulf_eq0 oppr_eq0 pnatr_eq0 orFb =>/eqP Hrez. rewrite Hrez expr0n mulr0 exprn_even_le0 //= in H. by rewrite Hrez (eqP H) expr0n add0r eqxx. rewrite Hrez H ltr_spaddl ?orbT // ?lt_def sqr_ge0 // sqrf_eq0. rewrite lt_def mulf_eq0 oppr_eq0 pnatr_eq0 orFb in Hrez. by case/andP : Hrez => ->. 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)