proposition: Lemma Rseq_sum_zip_compat_even : forall An Bn n, (Rseq_sum (Rseq_zip An Bn) (2 * S n) = Rseq_sum An (S n) + Rseq_sum Bn n)%R.
proof: Proof. intros An Bn n ; rewrite two_Sn, Rseq_sum_simpl, Rseq_sum_zip_compat_odd, Rseq_sum_simpl, <- two_Sn ; unfold Rseq_zip. case (n_modulo_2 (2 * S n)) ; intros [p Hp] ; [| apply False_ind ; lia]. assert (Hp' : p = S n) by lia ; subst ; ring. Qed.
imports: Lia Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rewrite_facts Rpser_def Rpser_def_simpl MyRIneq MyNat Lra