proposition: Lemma PackSeriesCV : forall {R : ConstructiveReals} (un : nat -> CRcarrier R) (N : nat) (a s : CRcarrier R), series_cv un s -> series_cv (fun n => match n with | O => a | _ => un (N + n)%nat end) (s - CRsum un N + a).
proof: Proof. intros. intros n. specialize (H n) as [k maj]. exists k. intros i H. destruct i. - inversion H. subst k. simpl. clear H. rewrite <- (CRplus_comm a). unfold CRminus. rewrite CRopp_plus_distr. rewrite <- CRplus_assoc. rewrite CRplus_opp_r. rewrite CRplus_0_l. rewrite CRabs_opp. specialize (maj N (Nat.le_0_l N)). rewrite CRabs_minus_sym in maj. exact maj. - rewrite decomp_sum. simpl. unfold CRminus. rewrite CRplus_comm. rewrite CRopp_plus_distr. rewrite CRplus_assoc. rewrite <- (CRplus_assoc (-a)). rewrite CRplus_opp_l. rewrite CRplus_0_l. rewrite CRopp_plus_distr. rewrite CRopp_involutive. rewrite (CRsum_eq (fun i : nat => un (N + S i)%nat) (fun i : nat => un (S N + i)%nat)). rewrite CRplus_assoc. rewrite <- sum_assoc. rewrite CRplus_comm. simpl in maj. apply maj. apply (Nat.le_trans k (S i)). assumption. simpl. apply le_n_S. rewrite Nat.add_comm. rewrite <- (Nat.add_0_r i). rewrite <- Nat.add_assoc. apply Nat.add_le_mono_l. apply Nat.le_0_l. intros. rewrite Nat.add_succ_r. reflexivity. apply le_n_S. apply Nat.le_0_l. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveCauchyAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions