fact: Definition domainInfiniteSumAbsIncReverse {R : ConstructiveReals} {X : Set} (fn : nat -> @PartialFunction R X) (x : X) : Domain (XinfiniteSumAbs fn) x -> forall n:nat, Domain (fn n) x := fun xD n => let (xn, _) := xD in xn n.
imports: List QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete