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