proposition: Lemma join_series : convergent x -> forall y, {k : nat | {N : nat | forall n, N <= n -> x n [=] y (n + k)}} -> convergent y.
proof: Proof. red in |- *; intros H y H0. elim H0; intros k Hk. elim Hk; intros N HN. clear Hk H0. red in |- *; intros e H0. elim (H (e [/]TwoNZ) (pos_div_two _ _ H0)); intros M HM. exists (S (Nat.max N M + k)); intros. rstepl (e [/]TwoNZ[+]e [/]TwoNZ). apply AbsSmall_wdr_unfolded with (seq_part_sum x (m - k) [-]seq_part_sum x (S (Nat.max N M + k) - k)). rstepr (seq_part_sum x (m - k) [-]seq_part_sum x M[+] (seq_part_sum x M[-]seq_part_sum x (S (Nat.max N M + k) - k))). apply AbsSmall_plus. apply HM. apply (fun p n m : nat => Nat.add_le_mono_l n m p) with k. rewrite (Nat.add_comm k (m- k)). rewrite Nat.sub_add. apply Nat.le_trans with (Nat.max N M + k); auto with arith. rewrite Nat.add_comm; auto with arith. apply Nat.le_trans with (S (Nat.max N M + k)); auto with arith. apply AbsSmall_minus. apply HM. apply (fun p n m : nat => Nat.add_le_mono_l n m p) with k. rewrite (Nat.add_comm k (S (Nat.max N M + k) - k)). rewrite Nat.sub_add. apply Nat.le_trans with (Nat.max N M + k); auto. rewrite Nat.add_comm; auto with arith. apply Nat.le_trans with (S (Nat.max N M + k)); auto with arith. unfold seq_part_sum in |- *. apply eq_transitive_unfolded with (Sum (S (Nat.max N M + k) - k) (pred (m - k)) x). unfold Sum, Sum1 in |- *. rewrite Nat.lt_succ_pred with (z := 0). algebra. lia. astepr (Sum (S (Nat.max N M + k)) (pred m) y). 2: unfold Sum, Sum1 in |- *. 2: rewrite Nat.lt_succ_pred with (z := 0). 2: algebra. 2: lia. replace (pred m) with (pred (m - k) + k). 2: lia. pattern (S (Nat.max N M + k)) at 2 in |- *; replace (S (Nat.max N M + k)) with (S (Nat.max N M + k) - k + k). 2: lia. apply Sum_big_shift. intros; apply HN. apply Nat.le_trans with (Nat.max N M); auto with arith. lia. rewrite Nat.lt_succ_pred with (z := 0); auto. lia. apply Nat.lt_le_trans with (S (Nat.max N M)); auto with arith. lia. Qed.
imports: CoRN.reals.CSumsReals CoRN.reals.NRootIR Coq(Lia)