proposition: Lemma abs_RInt_le_const : forall (f : R -> R) a b M, a <= b -> ex_RInt f a b -> (forall t, a <= t <= b -> Rabs (f t) <= M) -> Rabs (RInt f a b) <= (b - a) * M.
proof: Proof. intros f a b M Hab If H. apply: (norm_RInt_le_const f) => //. exact: RInt_correct. Qed.
imports: Coq(Reals Psatz) mathcomp(ssreflect ssrbool ssrfun eqtype seq) Markov Rcomplements Rbar Lub Lim_seq SF_seq Continuity Hierarchy