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