proposition: Lemma Rseq_sum_pos_strong : forall An n, (forall p, (p <= n)%nat -> 0 <= An p) -> 0 <= Rseq_sum An n.
proof: Proof. intros An n ; induction n ; intro Hpos. simpl ; apply Hpos ; trivial. rewrite Rseq_sum_simpl ; apply Rplus_le_le_0_compat ; [apply IHn ; intros p p_bd |] ; apply Hpos ; lia. Qed.
imports: Lia Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rewrite_facts Rpser_def Rpser_def_simpl MyRIneq MyNat Lra