proposition: Lemma to_algdom_exists (x : algcreal) : { y : algdom | (to_algcreal y == x)%CR }.
proof: Proof. pose p := annul_creal x. move: {2}(size p) (leqnn (size p))=> n. elim: n x @p=> [x p|n ihn x p le_sp_Sn]. by rewrite leqn0 size_poly_eq0 /p annul_creal_eq0. move: le_sp_Sn; rewrite leq_eqVlt. have [|//|eq_sp_Sn _] := ltngtP. by rewrite ltnS=> /ihn ihnp _; apply: ihnp. have px0 := @root_annul_creal x; rewrite -/p -/root in px0. have [|ncop] := boolP (coprimep p p^`()). move/coprimep_root => /(_ _ px0) /deriv_neq0_mono [r r_gt0 [i ir sm]]. have p_chg_sign : p.[x i - r] * p.[x i + r] <= 0. have [/accr_pos_incr hp|/accr_neg_decr hp] := sm. have hpxj : forall j, (i <= j)%N -> (p.[x i - r] <= p.[x j]) * (p.[x j] <= p.[x i + r]). move=> j hj. suff: p.[x i - r] <= p.[x j] <= p.[x i + r] by case/andP=> -> ->. rewrite !hp 1?addrAC ?subrr ?add0r ?normrN; rewrite ?(gtr0_norm r_gt0) //; do ?by rewrite ltW ?cauchymodP ?(leq_trans _ hj). by rewrite -ler_distl ltW ?cauchymodP ?(leq_trans _ hj). rewrite mulr_le0_ge0 //; apply/le_creal_cst; rewrite -px0; by apply: (@le_crealP _ i)=> h hj /=; rewrite hpxj. have hpxj : forall j, (i <= j)%N -> (p.[x i + r] <= p.[x j]) * (p.[x j] <= p.[x i - r]). move=> j hj. suff: p.[x i + r] <= p.[x j] <= p.[x i - r] by case/andP=> -> ->. rewrite !hp 1?addrAC ?subrr ?add0r ?normrN; rewrite ?(gtr0_norm r_gt0) //; do ?by rewrite ltW ?cauchymodP ?(leq_trans _ hj). by rewrite andbC -ler_distl ltW ?cauchymodP ?(leq_trans _ hj). rewrite mulr_ge0_le0 //; apply/le_creal_cst; rewrite -px0; by apply: (@le_crealP _ i)=> h hj /=; rewrite hpxj. pose y := (AlgDom (monic_annul_creal x) (ltW r_gt0) p_chg_sign). have eq_py_px: (p.[to_algcreal y] == p.[x])%CR. rewrite /to_algcreal -lock. by have := @to_algcrealP y; rewrite /= -/p=> ->; apply: eq_creal_sym. exists y. move: sm=> /strong_mono_bound [k k_gt0 hk]. rewrite -/p; apply: eq_crealP. exists_big_modulus m F. move=> e j e_gt0 hj; rewrite (le_lt_trans (hk _ _ _ _)) //. + rewrite /to_algcreal -lock. rewrite (le_trans (to_algcreal_ofP _ _ _ (leq0n _))) ?(ltW r_gt0) //. by rewrite expr0 divr1. + by rewrite ltW // cauchymodP. rewrite -ltr_pdivl_mull //. by rewrite (@eq_modP _ _ _ eq_py_px) // ?pmulr_rgt0 ?invr_gt0. by close. case: (@smaller_factor _ p p^`() x); rewrite ?monic_annul_creal //. rewrite gtNdvdp // -?size_poly_eq0 size_deriv eq_sp_Sn //=. apply: contra ncop=> /eqP n_eq0; move: eq_sp_Sn; rewrite n_eq0. by move=> /eqP /size_poly1P [c c_neq0 ->]; rewrite derivC coprimep0 polyC_eqp1. move=> r /andP [hsr monic_r rx_eq0]. apply: (ihn (AlgCReal monic_r rx_eq0))=> /=. by rewrite -ltnS -eq_sp_Sn. 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)