proposition: Lemma IntegralRepresentationWeaveSum : forall {IS : IntegrationSpace} (a b : @IntegralRepresentation IS), IntegralSeries (IntegralRepresentationWeave a b) == IntegralSeries a + IntegralSeries b.
proof: Proof. intros. apply (series_cv_unique (fun n => I IS (IntFn (IntegralRepresentationWeave a b) n) (IntFnL (IntegralRepresentationWeave a b) n) )). apply IntegralCv. simpl. apply (series_cv_eq (weaveSequences (CRcarrier (RealT (ElemFunc IS))) (fun n => I IS (IntFn a n) (IntFnL a n)) (fun n => I IS (IntFn b n) (IntFnL b n)))). intro n. unfold weaveSequences, weaveSequencesL. destruct (Nat.even n); reflexivity. apply weaveInfiniteSums; apply IntegralCv. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase