fact: Definition CRmorph_compose {R1 R2 R3 : ConstructiveReals} (f : @ConstructiveRealsMorphism R1 R2) (g : @ConstructiveRealsMorphism R2 R3) : @ConstructiveRealsMorphism R1 R3.
imports: QArith Qabs ConstructiveReals ConstructiveLimits ConstructiveAbs