proposition: Lemma rat_algebraic_archimedean (C : numFieldType) (QtoC : Qmorphism C) : integralRange QtoC -> Num.archimedean_axiom C.
proof: Proof. move=> algC x. without loss x_ge0: x / 0 <= x by rewrite -normr_id; apply. have [-> | nz_x] := eqVneq x 0; first by exists 1; rewrite normr0. have [p mon_p px0] := algC x; exists (\sum_(j < size p) `|numq p`_j|)%N. rewrite ger0_norm // real_ltNge ?rpred_nat ?ger0_real //. apply: contraL px0 => lb_x; rewrite rootE gt_eqF // horner_coef size_map_poly. have x_gt0 k: 0 < x ^+ k by rewrite exprn_gt0 // lt_def nz_x. move: lb_x; rewrite polySpred ?monic_neq0 // !big_ord_recr coef_map /=. rewrite -lead_coefE (monicP mon_p) natrD rmorph1 mul1r => lb_x. case: _.-1 (lb_x) => [|n]; first by rewrite !big_ord0 !add0r ltr01. rewrite -ltrBlDl add0r -(ler_pM2r (x_gt0 n)) -exprS. apply: lt_le_trans; rewrite mulrDl mul1r ltr_pwDr // -sumrN. rewrite natr_sum mulr_suml ler_sum // => j _. rewrite coef_map /= fmorph_eq_rat (le_trans (real_ler_norm _)) //. by rewrite rpredN rpredM ?rpred_rat ?rpredX // ger0_real. rewrite normrN normrM ler_pM //. rewrite normf_div -!intr_norm -!abszE ler_piMr ?ler0n //. by rewrite invf_le1 ?ler1n ?ltr0n absz_gt0. rewrite normrX ger0_norm ?(ltrW x_gt0) // ler_weXn2l ?leq_ord //. by rewrite (le_trans _ lb_x) // natr1 ler1n. 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)