proposition: Lemma str_Archimedes : forall x : IR, [0] [<=] x -> {n : nat | x [<=] nring n /\ (2 <= n -> nring n[-]Two [<=] x)}.
proof: Proof. intros. elim (Archimedes x); intros n Hn. induction n as [| n Hrecn]. exists 0; split; auto. intro; exfalso; lia. clear Hrecn. induction n as [| n Hrecn]. exists 1. split; intros; [ assumption | eapply leEq_transitive ]. 2: apply H. simpl in |- *. rstepl ([--]OneR); astepr ([--]ZeroR); apply less_leEq; apply inv_resp_less; apply pos_one. cut (nring (R:=IR) n [<] nring (S n)). intros H0. cut (nring n [<] x or x [<] nring (S n)). intros H1. elim H1; intros. exists (S (S n)). split. assumption. intros. simpl in |- *; rstepl (nring (R:=IR) n); apply less_leEq; assumption. apply Hrecn; apply less_leEq; assumption. apply less_cotransitive_unfolded; assumption. simpl in |- *; apply less_plusOne. Qed.
imports: CoRN.reals.CReals Coq(Lia)