fact: Definition PartialFunction {R : ConstructiveReals} (X : Set) : Type := @PartialFunctionXY X (CRcarrier R) (CReq R).
imports: List QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete