proposition: Lemma Rrepr_opp : forall x:R, Rrepr (- x) == - Rrepr x.
proof: Proof. intros. rewrite RbaseSymbolsImpl.Ropp_def, Rquot2. reflexivity. Qed.
imports: ZArith_base ClassicalDedekindReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveLUB Rdefinitions