proposition: Lemma odd_zeta_evens : Rser_cv (evens (Rseq_shift Rseq_square_inv)) (PI ^ 2 / 8).
proof: Proof. apply Rser_cv_ext with bntg. intro n. unfold Rseq_shift, evens, Rseq_square_inv, bntg. replace (INR (S (2 * n))) with (2 * INR n + 1); [reflexivity | ]. replace (S n) with (1 + n)%nat by reflexivity. INR_solve. do 2 (try rewrite <- plus_INR; try rewrite <- mult_INR). inject; lia. apply odd_zeta. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith