proposition: Lemma Rseq_sum_upper_bound : forall An n ub, (forall m, (m <= n)%nat -> An m <= ub) -> Rseq_sum An n <= INR (S n) * ub.
proof: Proof. intros An n ub HAn ; induction n. simpl ; rewrite Rmult_1_l ; apply HAn ; reflexivity. rewrite S_INR, Rmult_plus_distr_r, Rmult_1_l, Rseq_sum_simpl ; apply Rplus_le_compat ; [apply IHn | apply HAn ; reflexivity]. intros m m_lb ; apply HAn ; lia. Qed.
imports: Lia Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rewrite_facts Rpser_def Rpser_def_simpl MyRIneq MyNat Lra