fact: Definition domainXsumInc {R : ConstructiveReals} {X : Set} (fn : nat -> @PartialFunction R X) (x : X) (xn : forall n:nat, Domain (fn n) x) : forall n:nat, Domain (Xsum fn n) x.
imports: List QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete