proposition: Lemma aew_series_conv : convergent x -> convergent y.
proof: Proof. intro H. red in |- *; red in |- *; intros. rename X into H0. elim (H _ (pos_div_two _ _ H0)); intros N HN. elim aew_equal; intros n Hn. set (k := Nat.max (Nat.max n N) 1) in *. exists k; intros. apply AbsSmall_wdr_unfolded with (seq_part_sum x m[-]seq_part_sum x k). rstepr (seq_part_sum x m[-]seq_part_sum x N[+] (seq_part_sum x N[-]seq_part_sum x k)). rstepl (e [/]TwoNZ[+]e [/]TwoNZ). apply AbsSmall_plus. apply HN; cut (N <= k). lia. apply Nat.le_trans with (Nat.max n N); unfold k in |- *; auto with arith. apply AbsSmall_minus; apply HN; auto. apply Nat.le_trans with (Nat.max n N); unfold k in |- *; auto with arith. cut (1 <= k); intros. eapply eq_transitive_unfolded. apply seq_part_sum_n; auto. apply Nat.lt_le_trans with k; auto. eapply eq_transitive_unfolded. 2: apply eq_symmetric_unfolded; apply seq_part_sum_n; auto. 2: apply Nat.lt_le_trans with k; auto. apply Sum_wd'. rewrite Nat.lt_succ_pred with 0 m; auto with arith. apply Nat.lt_le_trans with k; auto. intros; apply Hn. apply Nat.le_trans with (Nat.max n N); auto with arith. apply Nat.le_trans with k; unfold k in |- *; auto with arith. unfold k in |- *; apply Nat.le_max_r. Qed.
imports: CoRN.reals.CSumsReals CoRN.reals.NRootIR Coq(Lia)