proposition: Lemma halfWeavedSumEven : forall {R : ConstructiveReals} (fn gn : nat -> CRcarrier R) (a : CRcarrier R), (forall k:nat, 0 <= fn k) -> (forall k:nat, 0 <= gn k) -> series_cv (weaveSequences (CRcarrier R) fn gn) a -> { l : CRcarrier R & series_cv fn l }.
proof: Proof. intros. destruct (series_cv_maj (weaveSequences (CRcarrier R) fn (fun n => 0)) (weaveSequences (CRcarrier R) fn gn) a) as [l [cv _]]. - intro n. unfold weaveSequences. destruct (Nat.even n). rewrite CRabs_right. apply CRle_refl. apply H. rewrite CRabs_right. apply H0. apply CRle_refl. - assumption. - exists l. intros n. specialize (cv n) as [N cv]. exists N. intros. specialize (cv (i*2)%nat). rewrite weaveSequencesSum in cv. rewrite Nat.div_mul in cv. setoid_replace (match (i * 2)%nat with | 0%nat => CR_of_Q R 0 | S _ => CRsum (fun _ : nat => 0) (if Nat.even (i * 2) then Init.Nat.pred i else i) end) with (CR_of_Q R 0) in cv. rewrite CRplus_0_r in cv. apply cv. apply (Nat.le_trans _ i). assumption. rewrite Nat.mul_comm. simpl. rewrite <- (Nat.add_0_r i). rewrite <- Nat.add_assoc. apply Nat.add_le_mono_l. apply Nat.le_0_l. destruct (i*2)%nat eqn:des. reflexivity. rewrite sum_const. rewrite CRmult_0_l. reflexivity. auto. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase