proposition: Lemma Rplus_reg_l : forall r r1 r2, r + r1 < r + r2 -> r1 < r2.
proof: Proof. intros. rewrite Rlt_def in H. apply CRealLtEpsilon in H. rewrite Rrepr_plus, Rrepr_plus in H. apply CReal_plus_lt_reg_l in H. rewrite Rlt_def. apply CRealLtForget. exact H. Qed.
imports: QArith_base Rdefinitions Raxioms ConstructiveReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveCauchyAbs ConstructiveRealsMorphisms