proposition: Lemma halfWeavedSumOdd : 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 gn l }.
proof: Proof. intros. destruct (series_cv_maj (weaveSequences (CRcarrier R) (fun n => 0) gn) (weaveSequences (CRcarrier R) fn gn) a) as [l [cv _]]. - intro n. unfold weaveSequences. destruct (Nat.even n). rewrite CRabs_right. apply H. apply CRle_refl. rewrite CRabs_right. apply CRle_refl. apply H0. - assumption. - exists l. intros p. specialize (cv p) as [N cv]. exists N. intros n H2. specialize (cv (1+n*2)%nat). rewrite weaveSequencesSum in cv. rewrite Nat.div_add in cv. rewrite sum_const in cv. rewrite CRmult_0_l in cv. rewrite CRplus_0_l in cv. destruct (1 + n*2)%nat eqn:des. + exfalso. inversion des. + rewrite <- des in cv. clear des. destruct (Nat.even (1+n*2)) eqn:des. exfalso. assert (Nat.Odd (1+n*2)). exists n. rewrite Nat.add_comm. rewrite Nat.mul_comm. reflexivity. apply Nat.odd_spec in H3. unfold Nat.odd in H3. rewrite des in H3. inversion H3. apply cv. apply (Nat.le_trans N n). assumption. apply (Nat.le_trans n (n*2)). rewrite <- (Nat.mul_1_r n). rewrite <- Nat.mul_assoc. apply Nat.mul_le_mono_nonneg_l. apply Nat.le_0_l. apply le_S. apply Nat.le_refl. rewrite <- (Nat.add_0_l (n*2)). rewrite Nat.add_assoc. apply Nat.add_le_mono_r. auto. + auto. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase