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