fact: Definition XsumList {R : ConstructiveReals} {X : Set} : list (@PartialFunction R X) -> PartialFunction X := fold_right Xplus (Xconst _ 0).
imports: List QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete