proposition: Lemma RiemannInt_const_bound : forall f a b l u (h : Riemann_integrable f a b), a <= b -> (forall x, a < x < b -> l <= f x <= u) -> l * (b - a) <= RiemannInt h <= u * (b - a).
proof: Proof. intros f a b l u ri ab intf. rewrite <- !(fun l => RiemannInt_P15 (RiemannInt_P14 a b l)). split; apply RiemannInt_P19; try assumption; intros x intx; unfold fct_cte; destruct (intf x intx); assumption. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra