fact: Definition Xconst {R : ConstructiveReals} (X : Set) (c : CRcarrier R) : PartialFunction X := Build_PartialFunctionXY X (CRcarrier R) (CReq R) (fun x => True) (fun x _ => c) (fun _ _ _ => CReq_refl c).
imports: List QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete