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