proposition: Lemma Sum_antg : Rser_cv antg (PI / 4).
proof: Proof. unfold Rser_cv. eapply Rseq_cv_eq_compat with (sum_f_R0 (tg_alt PI_tg)). 2: apply PI_tg_PI. apply Rseq_sum_ext. intros n. unfold tg_alt, PI_tg, antg. INR_group (2 * INR n + 1). field. INR_solve. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia