proposition: Lemma zeta2_half : Rser_cv (odds (Rseq_shift (Rseq_square_inv))) (zeta2 / 4).
proof: Proof. replace (zeta2 / 4) with (/4 * zeta2) by field. assert (REW : forall a, (/4 * (4 * a))%Rseq == a). intros a n; unfold Rseq_mult, Rseq_inv; field. unfold Rseq_constant. apply Rgt_not_eq ; lra. eapply Rser_cv_ext. symmetry ; apply REW. apply (Rser_cv_scal_compat_l _ _ (/ 4)). eapply Rser_cv_ext. 2:unfold zeta2. 2:destruct Rser_cv_square_inv as [l H]. 2:apply H. intro n. unfold Rseq_mult, odds, Rseq_shift, Rseq_square_inv, Rseq_constant. replace (S (S (2 * n))) with (mult 2 (S n)) by lia. replace (INR (2 * (S n))) with (2 * INR (S n)) by (rewrite mult_INR; trivial). unfold Rseq_square_inv_s. field. apply not_0_INR; lia. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith