proposition: Lemma rat_algebraic_decidable (C : fieldType) (QtoC : Qmorphism C) : integralRange QtoC -> decidable_embedding QtoC.
proof: Proof. have QtoCinj: injective QtoC by apply: fmorph_inj. pose ZtoQ : int -> rat := intr; pose ZtoC : int -> C := intr. have ZtoQinj: injective ZtoQ by apply: intr_inj. have defZtoC: ZtoC =1 QtoC \o ZtoQ by move=> m; rewrite /= rmorph_int. move=> algC x; have /sig2_eqW[q mon_q qx0] := algC x; pose d := (size q).-1. have [n ub_n]: {n | forall y, root q y -> `|y| < n}. have [n1 ub_n1] := monic_Cauchy_bound mon_q. have /monic_Cauchy_bound[n2 ub_n2]: (-1) ^+ d *: (q \Po - 'X) \is monic. rewrite monicE lead_coefZ lead_coef_comp ?size_opp ?size_polyX // -/d. by rewrite lead_coefN lead_coefX (monicP mon_q) (mulrC 1) signrMK. exists (Num.max n1 n2) => y; rewrite ltNge ler_normr !leUx rootE. apply: contraL => /orP[]/andP[] => [/ub_n1/gt_eqF->// | _ /ub_n2/gt_eqF]. by rewrite hornerZ horner_comp !hornerE opprK mulf_eq0 signr_eq0 => /= ->. have [p [a nz_a Dq]] := rat_poly_scale q; pose N := Num.bound `|n * a%:~R|. pose xa : seq rat := [seq (m%:R - N%:R) / a%:~R | m <- iota 0 N.*2]. have [/sig2_eqW[y _ ->] | xa'x] := @mapP _ _ QtoC xa x; first by left; exists y. right=> [[y Dx]]; case: xa'x; exists y => //. have{x Dx qx0} qy0: root q y by rewrite Dx fmorph_root in qx0. have /dvdzP[b Da]: (denq y %| a)%Z. have /Gauss_dvdzl <-: coprimez (denq y) (numq y ^+ d). by rewrite coprimez_sym coprimezXl //; apply: coprime_num_den. pose p1 : {poly int} := a *: 'X^d - p. have Dp1: p1 ^ intr = a%:~R *: ('X^d - q). by rewrite rmorphB /= linearZ /= map_polyXn scalerBr Dq scalerKV ?intr_eq0. apply/dvdzP; exists (\sum_(i < d) p1`_i * numq y ^+ i * denq y ^+ (d - i.+1)). apply: ZtoQinj; rewrite /ZtoQ rmorphM mulr_suml rmorph_sum /=. transitivity ((p1 ^ intr).[y] * (denq y ^+ d)%:~R). rewrite Dp1 !hornerE (rootP qy0) subr0. by rewrite !rmorphXn /= numqE exprMn mulrA. have sz_p1: (size (p1 ^ ZtoQ)%R <= d)%N. rewrite Dp1 size_scale ?intr_eq0 //; apply/leq_sizeP=> i. rewrite leq_eqVlt eq_sym -polySpred ?monic_neq0 // coefB coefXn. case: eqP => [-> _ | _ /(nth_default 0)->//]. by rewrite -lead_coefE (monicP mon_q). rewrite (horner_coef_wide _ sz_p1) mulr_suml; apply: eq_bigr => i _. rewrite -!mulrA -exprSr coef_map !rmorphM !rmorphXn /= numqE exprMn -mulrA. by rewrite -exprD -addSnnS subnKC. pose m := `|(numq y * b + N)%R|%N. have Dm: m%:R = `|y * a%:~R + N%:R|. by rewrite pmulrn abszE intr_norm Da rmorphD !rmorphM /= numqE mulrAC mulrA. have ltr_Qnat n1 n2 : (n1%:R < n2%:R :> rat = _) := ltr_nat _ n1 n2. have ub_y: `|y * a%:~R| < N%:R. apply: le_lt_trans (archi_boundP (normr_ge0 _)); rewrite !normrM. by rewrite ler_pM // (le_trans _ (ler_norm n)) ?ltW ?ub_n. apply/mapP; exists m. rewrite mem_iota /= add0n -addnn -ltr_Qnat Dm natrD. by rewrite (le_lt_trans (ler_normD _ _)) // normr_nat ltrD2. rewrite Dm ger0_norm ?addrK ?mulfK ?intr_eq0 // -lerBlDl sub0r. by rewrite (le_trans (ler_norm _)) ?normrN ?ltW. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq choice) mathcomp(div fintype path tuple bigop finset prime order) mathcomp(ssralg poly polydiv mxpoly countalg closed_field) mathcomp(ssrnum ssrint archimedean rat intdiv fingroup) mathcomp(finalg zmodp cyclic pgroup sylow vector falgebra) mathcomp(fieldext separable galois)