proposition: Lemma Rser_RiemannInt_link : { l | Rser_cv (fun n => f (INR n) - RiemannInt (Riemann_integrable_f_n_Sn n) ) l}.
proof: Proof. apply Rser_pos_bound_cv with (f 0). intro n. destruct (Rint_constant (f n) n (S n)) as [ pr int]. replace (f n * (S n -n)) with (f n) in int by (rewrite S_INR; ring). rewrite <- int. apply Rle_minus'. apply RiemannInt_P19; [intuition|]. intros x [xn snx]. assert(Hcond : 0 <= (INR n) <= x). split. auto with *. left; apply xn. apply (Hdec _ _ Hcond). intro n. apply Rle_trans with (sum_f_R0 (fun n => f (INR n) - f (INR (S n))) n). apply sum_Rle. intros i ni. destruct (Rint_constant (f i) i (S i)) as [ pr int]. replace (f i * (S i -i)) with (f i) in int by (rewrite S_INR; ring). rewrite <- int. rewrite <- RiemannInt_minus with _ _ _ _ _ _ (Rser_RiemannInt_link_general_term_integrable i); [|intuition]. rewrite RiemannInt_P15. replace (INR (S i) - INR i) with 1. rewrite Rmult_1_r. apply (Rser_RiemannInt_link_general_term_bound i). rewrite <- minus_INR by intuition. replace (S i - i)%nat with 1%nat by intuition. reflexivity. rewrite Telescoping_series_opp. rewrite <- Rminus_0_r. apply Rminus_le_compat_r. apply Hpos. auto with *. Qed.
imports: Reals Rseries_def Rseries_facts RiemannInt Lra Rsequence_facts Rsequence_subsequence Riemann_integrable Rintegral