proposition: Lemma Rser_pos_strictly_growing: forall Un, (forall n, 0 < Un n) -> Rseq_strictly_growing (Rseq_sum Un).
proof: Proof. intros Un Un_pos n ; apply Rle_lt_trans with (Rseq_sum Un n + 0)%R. rewrite Rplus_0_r ; reflexivity. apply Rplus_lt_compat_l ; trivial. Qed.
imports: Rsequence Rsequence_stdlib Rseries_def Rseries_base_facts