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