proposition: Lemma Rarchimedean : forall x y : R, x < y -> {q : Q & ((x < IQR q) * (IQR q < y))%type}.
proof: Proof. intros. rewrite Rlt_def in H. apply CRealLtEpsilon in H. apply CRealQ_dense in H. destruct H as [q [H2 H3]]. exists q. split. - rewrite Rlt_def. apply CRealLtForget. unfold IQR. rewrite Rquot2. exact H2. - rewrite Rlt_def. apply CRealLtForget. unfold IQR. rewrite Rquot2. exact H3. Qed.
imports: QArith_base Rdefinitions Raxioms ConstructiveReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveCauchyAbs ConstructiveRealsMorphisms