proposition: Lemma Rmult_pos : forall x y : R, IQR 0 < x -> IQR 0 < y -> IQR 0 < x * y.
proof: Proof. intros. rewrite Rlt_def. apply CRealLtForget. unfold IQR. rewrite Rquot2. rewrite Rrepr_mult. apply CReal_mult_lt_0_compat. - rewrite Rlt_def in H. apply CRealLtEpsilon in H. unfold IQR in H. rewrite Rquot2 in H. exact H. - unfold IQR in H0. rewrite Rlt_def in H0. apply CRealLtEpsilon in H0. rewrite Rquot2 in H0. exact H0. Qed.
imports: QArith_base Rdefinitions Raxioms ConstructiveReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveCauchyAbs ConstructiveRealsMorphisms