proposition: Lemma IQR_lt : forall n m:Q, (n < m)%Q -> IQR n < IQR m.
proof: Proof. intros. rewrite Rlt_def. apply CRealLtForget. unfold IQR. rewrite Rquot2, Rquot2. apply inject_Q_lt, H. Qed.
imports: QArith_base Rdefinitions Raxioms ConstructiveReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveCauchyAbs ConstructiveRealsMorphisms