proposition: Lemma RiemannInt_P14 : forall a b c:R, Riemann_integrable (fct_cte c) a b.
proof: Proof. unfold Riemann_integrable; intros; split with (mkStepFun (StepFun_P4 a b c)); split with (mkStepFun (StepFun_P4 a b 0)); split; [ intros; simpl; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; unfold fct_cte; right; reflexivity | 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