proposition: Lemma Rser_pos_growing: forall Un, (forall n, 0 <= Un n) -> Rseq_growing (Rseq_sum Un).
proof: Proof. intros Un Un_pos n ; transitivity (Rseq_sum Un n + 0)%R. rewrite Rplus_0_r ; reflexivity. apply Rplus_le_compat_l ; trivial. Qed.
imports: Rsequence Rsequence_stdlib Rseries_def Rseries_base_facts