proposition: Lemma is_RInt_le_0 : forall (f : R -> R) (a b If : R), a <= b -> is_RInt f a b If -> (forall x : R, a < x < b -> f x <= 0) -> If <= 0.
proof: Proof. move => f a b If leab fint fneg. suff: (0 <= -If) by lra. apply: (is_RInt_ge_0 (fun x => - (f x)) a b _ leab). exact: is_RInt_opp. by move => x Hx; move: (fneg x Hx); lra. Qed.
imports: Coq(Reals List Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool) Stdlib Coquelicot Xreal Interval Taylor_model Interval_compl