fact: Definition Rabs_quot (x : R) := Rabst (CReal_abs (Rrepr x)).
imports: QArith_base Rdefinitions Raxioms ConstructiveReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveCauchyAbs ConstructiveRealsMorphisms