proposition: Lemma norm_RInt_le_const_abs : forall (f : R -> V) (a b : R) (lf : V) (M : R), (forall x, Rmin a b <= x <= Rmax a b -> norm (f x) <= M) -> is_RInt f a b lf -> norm lf <= Rabs (b - a) * M.
proof: Proof. intros f a b lf M H Hf. unfold Rabs. case Rcase_abs => Hab. apply Rminus_lt in Hab. rewrite Ropp_minus_distr. apply is_RInt_swap in Hf. rewrite <- norm_opp. apply norm_RInt_le_const with (3 := Hf). now apply Rlt_le. intros x Hx. apply H. now rewrite -> Rmin_right, Rmax_left by now apply Rlt_le. apply Rminus_ge in Hab. apply Rge_le in Hab. apply norm_RInt_le_const with (1 := Hab) (3 := Hf). intros x Hx. apply H. now rewrite -> Rmin_left, Rmax_right. Qed.
imports: Coq(Reals Psatz) mathcomp(ssreflect ssrbool ssrfun eqtype seq) Markov Rcomplements Rbar Lub Lim_seq SF_seq Continuity Hierarchy