proposition: Lemma abs_RInt_le : forall (f : R -> R) a b, a <= b -> ex_RInt f a b -> Rabs (RInt f a b) <= RInt (fun t => Rabs (f t)) a b.
proof: Proof. intros f a b H1 If. apply: (norm_RInt_le f (fun t : R => norm (f t)) a b). exact H1. move => x _ ; by apply Rle_refl. exact: RInt_correct. apply: RInt_correct. exact: ex_RInt_norm. Qed.
imports: Coq(Reals Psatz) mathcomp(ssreflect ssrbool ssrfun eqtype seq) Markov Rcomplements Rbar Lub Lim_seq SF_seq Continuity Hierarchy