proposition: Lemma zeta2_val : zeta2 = PI ^ 2 / 6.
proof: Proof. apply Rmult_eq_reg_l with (3 / 4); [ | intro H; apply (Rmult_eq_compat_l 4) in H; field_simplify in H; lra]. replace (3 / 4 * zeta2) with (zeta2 - zeta2 / 4) by field. replace (3 / 4 * (PI ^ 2 / 6)) with (PI ^ 2 / 8) by field. eapply Rser_cv_unique. apply Rser_cv_minus_compat. unfold zeta2. destruct Rser_cv_square_inv as [x H]. apply H. 2:apply remove_odds. apply zeta2_half. apply Rser_cv_square_inv. apply odd_zeta_evens. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith