proposition: Lemma Rmult_lt_compat_l : forall r r1 r2:R, 0 < r -> r1 < r2 -> r * r1 < r * r2.
proof: Proof. intros. rewrite RbaseSymbolsImpl.Rlt_def. rewrite RbaseSymbolsImpl.Rlt_def in H. do 2 rewrite Rrepr_mult. apply CRealLtForget. apply CReal_mult_lt_compat_l. - rewrite <- (Rquot2 0%CReal). unfold IZR in H. rewrite RbaseSymbolsImpl.R0_def in H. apply CRealLtEpsilon. exact H. - rewrite RbaseSymbolsImpl.Rlt_def in H0. apply CRealLtEpsilon. exact H0. Qed.
imports: ZArith_base ClassicalDedekindReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveLUB Rdefinitions