proposition: Lemma Rabove_pos : forall x : R, {n : positive & x < IQR (Z.pos n # 1)}.
proof: Proof. intros. destruct (Rup_nat (Rrepr x)) as [n nmaj]. exists (Pos.of_nat n). unfold IQR. rewrite Rlt_def, Rquot2. apply CRealLtForget. apply (CReal_lt_le_trans _ _ _ nmaj). apply inject_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_r. destruct n. - discriminate. - rewrite <- positive_nat_Z. rewrite Nat2Pos.id. + apply Z.le_refl. + discriminate. Qed.
imports: QArith_base Rdefinitions Raxioms ConstructiveReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveCauchyAbs ConstructiveRealsMorphisms