proposition: Lemma pi_tg2_cv : { l | Rser_cv pi_tg2 l }.
proof: Proof. destruct (exist_PI) as [PI_4 Hc]. exists PI_4. apply Rser_cv_ext with (fun n => tg_alt PI_tg (2 * n) + tg_alt PI_tg (S (2 * n))). intro n; apply pi_tg2_corresp. apply Rser_cv_pair_compat. intros eps epspos. destruct (Hc eps epspos) as [N H]. exists N. intros n nN. apply (H n nN). Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia