proposition: Lemma bound2c_cv : Rseq_cv bound2c 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 => / INR (S n0)) (pred N)) 0). apply (half_mean_0 _ 1). lra. lia. intro; apply Rlt_le; apply Rinv_0_lt_compat; INR_solve. intro; unfold Rdiv; rewrite Rmult_1_l; apply Rle_Rinv; INR_solve. intros e epos; destruct (H e epos) as [N J]; exists N; intros n nN. simpl pred. unfold bound2c. replace (sum_f_R0 (fun n0 : nat => / INR (S n - S n0 + 1)) (pred (S n))) with (sum_f_R0 (fun n0 : nat => / INR (S n0)) (pred (S n))) by (rewrite <- Rsum_switch_index; apply Rseq_sum_ext; intro; inject; lia). apply J; lia. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith