proposition: Lemma to_algcrealP (x : algdom) : ((annul_algdom x).[alg_to_creal x] == 0)%CR.
proof: Proof. set u := alg_to_creal _; set p := annul_algdom _. pose r := radius_alg x; pose cr := cst_creal r. have: ((p).[u - cr * exp2k_creal] * (p).[u + cr * exp2k_creal] <= 0)%CR. apply: (@le_crealP _ 0%N)=> i _ /=. rewrite -/p -/r; set c := center_alg _. elim: i=> /= [|i]. by rewrite !expr0 divr1 algdomP. set c' := to_algcreal_of _ _ _=> ihi. have [] := lerP (_ * p.[c' i]). rewrite addrNK -addrA -opprD -mulr2n -[_ / _ *+ _]mulr_natr. by rewrite -mulrA exprSr invfM mulfVK ?pnatr_eq0. rewrite addrK -addrA -mulr2n -[_ / _ *+ _]mulr_natr. rewrite -mulrA exprSr invfM mulfVK ?pnatr_eq0 // => /ler_pmul2l<-. rewrite mulr0 mulrCA !mulrA [X in X * _]mulrAC -mulrA. by rewrite mulr_ge0_le0 // -expr2 exprn_even_ge0. rewrite exp2k_creal_eq0 mul_creal0 opp_creal0 add_creal0. move=> hu pu0; apply: hu; pose e := (lbound pu0). pose_big_enough i. apply: (@lt_crealP _ (e * e) i i) => //. by rewrite !pmulr_rgt0 ?invr_gt0 ?ltr0n ?lbound_gt0. rewrite add0r [u]lock /= -!expr2. rewrite -[_.[_] ^+ _]ger0_norm ?exprn_even_ge0 // normrX. rewrite ler_pexpn2r -?topredE /= ?lbound_ge0 ?normr_ge0 //. by rewrite -lock (le_trans _ (lbound0_of pu0)). by close. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrnum ssrint rat poly polydiv polyorder) mathcomp(perm matrix mxpoly polyXY binomial generic_quotient) mathcomp(cauchyreals separable zmodp bigenough)