proposition: Lemma Rseq_sum_pos: forall An n, (forall n, 0 <= An n) -> 0 <= Rseq_sum An n.
proof: Proof. intros ; apply Rseq_sum_pos_strong ; trivial. Qed.
imports: Lia Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rewrite_facts Rpser_def Rpser_def_simpl MyRIneq MyNat Lra