proposition: Lemma Rzero_lt_one : IQR 0 < IQR 1.
proof: Proof. rewrite Rlt_def. apply CRealLtForget. unfold IQR. rewrite Rquot2, Rquot2. apply CRealLt_0_1. Qed.
imports: QArith_base Rdefinitions Raxioms ConstructiveReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveCauchyAbs ConstructiveRealsMorphisms