proposition: Lemma Rseq_pps_zip_compat_even : forall An Bn x n, (Rseq_pps (Rseq_zip An Bn) x (2 * S n) = Rseq_pps An (x ^ 2) (S n) + x * Rseq_pps Bn (x ^ 2) n)%R.
proof: Proof. intros An Bn x n ; unfold Rseq_pps ; erewrite Rseq_sum_ext ; [| eapply gt_pser_zip_compat] ; rewrite Rseq_sum_zip_compat_even, Rseq_sum_scal_compat_l ; reflexivity. Qed.
imports: Lia Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rewrite_facts Rpser_def Rpser_def_simpl MyRIneq MyNat Lra