proposition: Lemma Rplus_0_l : forall r:R, 0 + r = r.
proof: Proof. intros. apply Rquot1. rewrite Rrepr_plus, Rrepr_0. apply CReal_plus_0_l. Qed.
imports: ZArith_base ClassicalDedekindReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveLUB Rdefinitions