proposition: Lemma IntegralRepresentationAbsVal : forall {IS : IntegrationSpace} (fInt : @IntegralRepresentation IS), IntegralSeries (IntegralRepresentationAbs fInt) == IntAbsSum fInt.
proof: Proof. intros. apply (CR_cv_unique (CRsum (fun n => Iabs (IntFn fInt n) (IntFnL fInt n)))). exact (IntegralCv (IntegralRepresentationAbs fInt)). apply fInt. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase