proposition: Lemma An_cv : Rseq_cv An (PI / 2).
proof: Proof. replace (PI / 2) with (PI / 4 + (PI / 4 + 1 - 1)) by field. eapply Rseq_cv_eq_compat. 2: apply Rseq_cv_plus_compat. 2: apply Sum_antg. 2: eapply Rseq_cv_eq_compat. 3: apply Rseq_cv_minus_compat. 3: apply Sum_antg_neg. 3: apply Rseq_constant_cv. symmetry. apply bisum_anz_antg. intro; trivial. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith