proposition: Lemma Rser_pos_bound_cv : forall Un M, (forall n, 0 <= Un n) -> Rser_bound_max Un M -> { l | Rser_cv Un l }.
proof: Proof. intros Un M Un_pos Hb ; destruct ub_to_lub with (Rseq_sum Un) as [l Hl]. eapply Rseq_bound_max_has_ub ; eassumption. exists l ; try apply tech10; apply Un_cv_crit_lub ; [apply Rser_pos_growing |] ; assumption. Qed.
imports: Rsequence Rsequence_stdlib Rseries_def Rseries_base_facts