proposition: Lemma CSUCIntegralAdditiveIterate : forall {R : ConstructiveReals} (fn : nat -> @PartialFunction R (X ElemCSUC)) (fnL : forall n : nat, L ElemCSUC (fn n)) (N : nat), IntegralCSUC (Xsum fn N) (LsumStable fn fnL N) == CRsum (fun n : nat => IntegralCSUC (fn n) (fnL n)) N.
proof: Proof. induction N. - reflexivity. - simpl. rewrite <- IHN. rewrite CSUCIntegralAdditive. reflexivity. Qed.
imports: QArith Qminmax Qpower Qabs ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions ConstructiveUniformCont ConstructiveCauchyIntegral CMTbase CMTPositivity CMTIntegrableFunctions CMTFullSets CMTIntegrableSets