proposition: Lemma Archimedes : forall x : R1, {n : nat | x [<=] nring n}.
proof: Proof. elim CReals_is_CReals. intros. apply ax_Arch. Qed.
imports: CoRN.model.reals.Cauchy_IR CoRN.model.monoids.Nmonoid CoRN.model.rings.Zring CoRN.algebra.CRing_Homomorphisms CoRN.algebra.Expon Coq.QArith.Qpower CoRN.tactics.CornTac