proposition: Theorem R_is_archemaedian : forall x : R_COrdField', {n : nat | x [<=] nring n}.
proof: Proof. intros. case x. intros x_ px. elim (px [1] (pos_one _)); intros Nx HNx. elim (F_is_archemaedian (x_ Nx)); intros N HN. exists (S N). intro H. elim H; intros K HK; elim HK; clear H HK; intros e He HK; simpl in HK. apply (less_irreflexive_unfolded F [0]). apply less_leEq_trans with e; auto. astepr (x_ (K + Nx) [-]x_ (K + Nx)). eapply leEq_transitive. apply (HK (K + Nx)); eauto with arith. unfold cg_minus in |- *; apply plus_resp_leEq_lft; apply inv_resp_leEq. rstepl (x_ Nx[+] (x_ (K + Nx) [-]x_ Nx)). apply plus_resp_leEq_both. apply leEq_wdr with (CS_seq _ (inject_Q (nring N)) (K + Nx)). simpl in |- *; apply less_leEq; auto. apply eq_symmetric_unfolded; apply ing_nring'. elim (HNx (K + Nx)); auto with arith. Qed.
imports: CoRN.algebra.Cauchy_COF CoRN.reals.CReals