proposition: Lemma tail_series : forall y, convergent y -> {k : nat | {N : nat | forall n, N <= n -> x n [=] y (n + k)}} -> convergent x.
proof: Proof. red in |- *. intros y H 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)); intros. rstepl (e [/]TwoNZ[+]e [/]TwoNZ). apply AbsSmall_wdr_unfolded with (seq_part_sum y (m + k) [-]seq_part_sum y (S (Nat.max N M) + k)). rstepr (seq_part_sum y (m + k) [-]seq_part_sum y M[+] (seq_part_sum y M[-]seq_part_sum y (S (Nat.max N M) + k))). apply AbsSmall_plus. apply HM. apply Nat.le_trans with (Nat.max N M); auto with arith. apply AbsSmall_minus. apply HM. auto with arith. unfold seq_part_sum in |- *. apply eq_transitive_unfolded with (Sum (S (Nat.max N M) + k) (pred (m + k)) y). unfold Sum, Sum1 in |- *. rewrite Nat.lt_succ_pred with (z := 0). algebra. apply Nat.lt_le_trans with (S (Nat.max N M)); auto with arith. astepr (Sum (S (Nat.max N M)) (pred m) x). 2: unfold Sum, Sum1 in |- *. 2: rewrite -> Nat.lt_succ_pred with (z := 0). 2: algebra. 2: apply Nat.lt_le_trans with (S (Nat.max N M)); auto with arith. replace (pred (m + k)) with (pred m + k). apply eq_symmetric_unfolded; apply Sum_big_shift. intros; apply HN. apply Nat.le_trans with (Nat.max N M); auto with arith. rewrite -> Nat.lt_succ_pred with (z := 0); auto. 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)