fact: Parameter Rplus_def : forall x y : R, Rplus x y = Rabst (CReal_plus (Rrepr x) (Rrepr y)).
imports: ZArith_base QArith_base ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ClassicalDedekindReals