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