proposition: Lemma IadditiveIterate : forall {IS : IntegrationSpace} (fn : nat -> PartialFunction (X (ElemFunc IS))) (fnL : forall n:nat, L (ElemFunc IS) (fn n)) (N : nat), I IS (Xsum fn N) (LsumStable fn fnL N) == CRsum (fun n : nat => I IS (fn n) (fnL n)) N.
proof: Proof. induction N. - reflexivity. - simpl. rewrite Iadditive. rewrite IHN. reflexivity. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions