proposition: Lemma Rint_generalized_Chasles : forall f An, (forall n : nat, Rint f n (S n) (An n)) -> forall n : nat, Rint f 0 (S n) (sum_f_R0 An n).
proof: Proof. intros f An H. induction n. apply (H O). apply Rint_Chasles with (S n). apply IHn. apply H. Qed.
imports: Reals Rseries_def Rseries_facts RiemannInt Lra Rsequence_facts Rsequence_subsequence Riemann_integrable Rintegral