proposition: Lemma Bn_cv : Rseq_cv Bn (PI ^ 2 / 4).
proof: Proof. replace (PI ^ 2 / 4) with (PI ^ 2 / 4 - 0) by field. apply Rseq_cv_eq_compat with (An * An - (An * An - Bn))%Rseq. intro; unfold Rseq_minus, Rseq_mult; ring. apply Rseq_cv_minus_compat. apply An_squared_cv. apply An_squared_Bn_cv. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith