proposition: Lemma normal_root_inB : forall (p : {poly R}), p \is monic -> (forall z : C, root (toC p) z -> inB z) -> p \is normal.
proof: Proof. move=> p Hpmonic. move: {2}(size p) (leqnn (size p))=> n. elim: n p Hpmonic=> [p Hpmonic Hpsize Hproot | n IH p Hpmonic Hpsize Hproots]. rewrite size_poly_leq0 in Hpsize. rewrite (eqP Hpsize) monicE lead_coef0 in Hpmonic. by rewrite (eqP Hpsize) normalE polyseq0 /= -(oner_eq0 R) eq_sym. case: (altP (size (toC p) =P 1%N)) => Hpsize2. rewrite monicE in Hpmonic. rewrite /= size_map_poly_id0 in Hpsize2; last by rewrite eq_sym negbT // lt_eqF // ltcR (eqP Hpmonic) ltr01. have Hp := (size1_polyC (eq_leq (Hpsize2))). rewrite Hp in Hpsize2. rewrite Hp lead_coefE Hpsize2 -pred_Sn polyseqC in Hpmonic. rewrite size_polyC in Hpsize2. rewrite Hpsize2 /= in Hpmonic. by rewrite Hp /= (eqP Hpmonic) normalE polyseqC oner_neq0 /= ltr01. move/closed_rootP : Hpsize2. case=> x Hrootx. case: (altP (Im x =P 0)) => Himx. have H := monicXsubC (Re x). have Hp := real_root_div_poly_deg1 Himx Hrootx. rewrite Pdiv.IdomainMonic.dvdp_eq // in Hp. rewrite (eqP Hp) normal_mulr //. apply: IH => [ | | z Hz]. + by rewrite monicE -(@lead_coef_Mmonic _ _ ('X - (Re x)%:P)) // -(eqP Hp) -monicE. - rewrite size_divp; last by apply: monic_neq0. by rewrite size_XsubC leq_subLR addnC addn1. + rewrite Hproots // (eqP Hp) rmorphM rootM. apply/orP; by left. rewrite monicXsubC_normal. rewrite /inB in Hproots. by have/andP := (Hproots x Hrootx); case => -> _. have H : 'X^2 + (1 *- 2 * Re x) *: 'X + (Re x ^+ 2 + Im x ^+ 2)%:P \is monic. by rewrite -(mul1r 'X^2) mul_polyC monicE lead_coefE polyseq_deg2 // oner_neq0. have H2 : size ('X^2 + (1 *- 2 * Re x) *: 'X + (Re x ^+ 2 + Im x ^+ 2)%:P) = 3%N. by rewrite -(mul1r 'X^2) mul_polyC polyseq_deg2 // oner_neq0. have Hp := complex_root_div_poly_deg2 Himx Hrootx. rewrite Pdiv.IdomainMonic.dvdp_eq // in Hp. rewrite (eqP Hp) normal_mulr //. apply: IH => [ | | z Hz]. + by rewrite monicE -(@lead_coef_Mmonic _ _ ('X^2 + (1 *- 2 * Re x) *: 'X + (Re x ^+ 2 + Im x ^+ 2)%:P)) // -(eqP Hp) -monicE. - rewrite size_divp; last by apply: monic_neq0. by rewrite H2 leq_subLR addnC addn2 (@leq_trans n.+1). + rewrite Hproots // (eqP Hp) rmorphM rootM. apply/orP; by left. by rewrite quad_monic_normal Hproots. 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)