proposition: Lemma Rser_RiemannInt_link_general_term_bound (n : nat) : RiemannInt (Rser_RiemannInt_link_general_term_integrable n) <= f (INR n) - f (INR (S n)).
proof: Proof. intros. rewrite <- Rmult_1_r. replace 1 with (INR (S n) - (INR n)). assert (pr:Riemann_integrable (fct_cte (f (INR n) - f (INR (S n)))) (INR n) (INR (S n))) by apply RiemannInt_P14. rewrite <- RiemannInt_P15 with _ _ _ pr. apply RiemannInt_P19; [intuition|]. unfold fct_cte. intros x [xn xsn]. apply Rminus_le_compat_r. apply Hdec. split. apply Rle_trans with (INR n). auto with *. left; apply xn. apply (Rlt_le _ _ xsn). rewrite <- minus_INR by intuition. replace (S n - n)%nat with 1%nat by intuition. reflexivity. Qed.
imports: Reals Rseries_def Rseries_facts RiemannInt Lra Rsequence_facts Rsequence_subsequence Riemann_integrable Rintegral