proposition: Lemma Sum_antg_neg : Rser_cv antg_neg (PI / 4 + 1).
proof: Proof. apply Rser_cv_shift_rev2. eapply Rser_cv_ext. apply antg_shift_neg_compat. replace (PI / 4 + 1 - antg_neg 0) with (PI / 4) by (compute; field). apply Sum_antg. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia