proposition: Lemma remove_odds : forall Un l, {lu | Rser_cv Un lu} -> Rser_cv (evens Un) l -> Rser_cv (Un - (odds Un)) l.
proof: Proof. intros Un lo [lu Hu] Ho. replace lo with (lu - (lu - lo)) by ring. apply Rser_cv_minus_compat; try assumption. apply Rseq_cv_eq_compat with ((fun n => sum_f_R0 Un (S (2 * n))) - sum_f_R0 (evens Un))%Rseq. intro n; rewrite (sum_odd_even_split); trivial. apply Rseq_cv_minus_compat. eapply Rseq_subseq_cv_compat; [|apply Hu]. assert (Hex : is_extractor (fun i => S (2 * i))). intros n; lia. exists (exist _ _ Hex). reflexivity. assumption. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia