proposition: Lemma Rser_cv_growing_subseq_compat: forall (An : Rseq) (phi : extractor) l, (forall n, 0 <= An n) -> Rseq_cv ((Rseq_sum An) ⋅ phi)%Rseq l -> Rser_cv An l.
proof: Proof. intros An phi l A_pos Hcv ; apply Rseq_subseq_growing_cv_compat with ((Rseq_sum An) ⋅ phi). exists phi ; trivial. assumption. intro ; transitivity (Rseq_sum An n + 0)%R. rewrite Rplus_0_r ; reflexivity. simpl ; apply Rplus_le_compat_l ; trivial. Qed.
imports: Rsequence Rsequence_stdlib Rseries_def Rseries_base_facts