proposition: Lemma RiemannInt_P7 : forall (f:R -> R) (a:R), Riemann_integrable f a a.
proof: Proof. unfold Riemann_integrable; intro f; intros; split with (mkStepFun (StepFun_P4 a a (f a))); split with (mkStepFun (StepFun_P4 a a 0)); split. - intros; simpl; unfold fct_cte; replace t with a. + unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; right; reflexivity. + generalize H; unfold Rmin, Rmax; decide (Rle_dec a a) with (Rle_refl a). intros (?,?); apply Rle_antisym; assumption. - rewrite StepFun_P18; rewrite Rmult_0_l; rewrite Rabs_R0; apply (cond_pos eps). Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra