proposition: Lemma Rser_RiemannInt_link_general_term_integrable : forall (n : nat), Riemann_integrable (fun x => fct_cte (f (INR n)) x - f x) (INR n) (INR (S n)).
proof: Proof. intros n. apply RiemannInt_integrable_minus. apply RiemannInt_P6. auto with *. intros x Hx. apply continuity_const. intros y z; reflexivity. apply (Riemann_integrable_f_n_Sn n). Qed.
imports: Reals Rseries_def Rseries_facts RiemannInt Lra Rsequence_facts Rsequence_subsequence Riemann_integrable Rintegral