proposition: Lemma Rseq_cv_inv_INR_0_1 : Rseq_cv (fun n => - / (2 * INR n + 1))%R 0%R.
proof: Proof. replace 0 with (-0)%R by intuition. apply Rseq_cv_opp_compat. generalize RinvN_cv. intros useful. intros eps Heps; destruct (Rseq_cv_inv_INR eps Heps) as (N, Hun). exists N. intros n Hn. generalize (Hun n Hn) ; intros Hun1. apply Rle_lt_trans with (/INR (n + 1))%R. unfold R_dist. rewrite Rminus_0_r. rewrite Rabs_pos_eq. apply Rle_Rinv. generalize (pos_INR n) ; intros ; rewrite plus_INR ; intuition. generalize (pos_INR n) ; intros ; lra. rewrite plus_INR. simpl. apply Rplus_le_compat_r. replace (INR n)%R with ((INR n ) * 1)%R by ring. rewrite Rmult_comm. apply Rmult_le_compat. intuition. apply pos_INR. intuition. intuition. left. apply Rinv_0_lt_compat. generalize (pos_INR n) ; intros ; lra. unfold R_dist in Hun1. rewrite Rminus_0_r in Hun1. rewrite Rabs_right in Hun1. apply Hun1. left. apply Rgt_lt. apply Rinv_0_lt_compat. intuition. Qed.
imports: PeanoNat Reals Rintegral Rintegral_usual Rintegral_tactic Lia Lra Rsequence_facts Rsequence_subsequence Rpser RTaylor MyRfunctions Rsequence_tactics