proposition: Lemma Rseq_sum_even_odd_split' : forall An n, (Rseq_sum (fun i => An (2 * i)%nat) (S n) + Rseq_sum (fun i => An (S (2 * i))) n = Rseq_sum An (2 * (S n)))%R.
proof: Proof. intros An n ; replace (2 * S n)%nat with (S (S (2 * n))) by ring ; do 2 rewrite Rseq_sum_simpl ; rewrite <- Rseq_sum_even_odd_split ; replace (2 * S n)%nat with (S (S (2 * n))) by ring ; ring. Qed.
imports: Lia Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rewrite_facts Rpser_def Rpser_def_simpl MyRIneq MyNat Lra