proposition: Lemma Riemann_integrable_f_n_Sn : forall (n : nat), Riemann_integrable f (INR n) (INR (S n)).
proof: Proof. intro n. apply continuity_implies_RiemannInt. apply le_INR; do 2 constructor. intros x [Hnx HxSn]; apply Hcont. apply (Rle_trans 0 (INR n) x (le_INR _ _ (Nat.le_0_l n)) Hnx). Qed.
imports: Reals Rseries_def Rseries_facts RiemannInt Lra Rsequence_facts Rsequence_subsequence Riemann_integrable Rintegral