proposition: Lemma An_squared_cv : Rseq_cv (An * An) (PI ^ 2 / 4).
proof: Proof. replace (PI ^ 2 / 4) with ((PI / 2) * (PI / 2)) by field. apply Rseq_cv_mult_compat; apply An_cv. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith