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