proposition: Lemma Rser_pos_cv_dec : (exists l, Rser_cv Un l) \/ (Rser_cv_pos_infty Un).
proof: Proof. destruct (classic (exists l, Rser_cv Un l)) as [yes | no]. left ; exact yes. right ; apply Rseq_unbounded_growing. apply NNPP. apply Rser_pos_growing ; assumption. intros [M HM] ; apply no ; destruct (Rser_pos_bound_cv _ _ Un_pos HM) as [l Hl] ; exists l ; assumption. Qed.
imports: Rsequence Rsequence_stdlib Rseries_def Rseries_base_facts