proposition: Theorem zeta2_pi_2_6 : Rser_cv (fun n => 1 / (n + 1) ^ 2) (PI ^ 2 / 6).
proof: Proof. rewrite <- zeta2_val. unfold zeta2. eapply Rser_cv_ext. 2:destruct Rser_cv_square_inv as [l H]. 2:apply H. intro n; unfold Rseq_shift, Rseq_square_inv_s. rewrite plus_1_S. field. INR_solve. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith