proposition: Lemma Rser_even_odd_split : forall An le lo, Rser_cv (fun n => An (2*n)%nat) le -> Rser_cv (fun n => An (S(2*n))%nat) lo -> Rser_cv An (le + lo).
proof: Proof. intros An le lo Hle Hlo ; apply Rseq_cv_even_odd_compat. apply Rseq_cv_shift_compat ; unfold Rseq_shift ; apply Rseq_cv_eq_compat with (Rseq_plus (Rseq_shift (Rseq_sum (fun i => An (2 * i)%nat))) (Rseq_sum (fun i => An (S (2 * i))))). intro n ; rewrite <- Rseq_sum_even_odd_split' ; unfold Rseq_shift, Rseq_plus ; reflexivity. apply Rseq_cv_plus_compat ; [apply Rseq_cv_shift_compat_reciprocal |] ; assumption. apply Rseq_cv_eq_compat with (Rseq_plus (Rseq_sum (fun i => An (2 * i)%nat)) (Rseq_sum (fun i => An (S (2 * i))))). intro n ; symmetry ; apply Rseq_sum_even_odd_split. apply Rseq_cv_plus_compat ; assumption. Qed.
imports: Rsequence Rseries_def Rseries_base_facts Rseries_pos_facts MyNat MyRIneq PeanoNat Lra Rtactic