proposition: Lemma Archimedes' : forall x : IR, {n : nat | x [<] nring n}.
proof: Proof. intro x. elim (Archimedes (x[+][1])); intros n Hn. exists n. apply less_leEq_trans with (x[+][1]); auto. apply less_plusOne. Qed.
imports: CoRN.reals.CReals Coq(Lia)