proposition: Lemma Rseq_cv_inv_INR : Rseq_cv (fun n => /INR (n + 1)) 0.
proof: Proof. generalize RinvN_cv. intros useful. intros eps Heps. destruct (useful eps Heps) as (N, H). exists N. intros n Hn. generalize (H n Hn). intros H1. unfold pos in H1. simpl in H1. rewrite plus_INR. apply H1. Qed.
imports: PeanoNat Reals Rintegral Rintegral_usual Rintegral_tactic Lia Lra Rsequence_facts Rsequence_subsequence Rpser RTaylor MyRfunctions Rsequence_tactics