fact: Definition Rabst_morphism : @ConstructiveRealsMorphism CRealConstructive DRealConstructive.
imports: QArith_base Rdefinitions Raxioms ConstructiveReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveCauchyAbs ConstructiveRealsMorphisms