proposition: Lemma bound2'_cv : Rseq_cv bound2' 0.
proof: Proof. apply Rseq_cv_shift_compat. unfold bound1', Rseq_shift. assert (Rseq_cv (fun N : nat => / INR (2 * N + 3) * sum_f_R0 (fun n0 : nat => 2 / INR (2 * n0 + 3)) (pred N)) 0). apply (half_mean_0 _ 2). lra. lia. intro; unfold Rdiv; apply Rle_mult_inv_pos; [lra | INR_solve]. intro; unfold Rdiv. apply Rmult_le_compat_l; [lra | ]. apply Rle_Rinv; INR_solve. intros e epos; destruct (H e epos) as [N J]; exists N; intros n nN. simpl pred. apply J; lia. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith