proposition: Lemma Rmonot_contains (g : R -> R) : Rmonot dom g -> forall (x y z : R), dom x -> dom y -> intvl x y z -> intvl (g x) (g y) (g z) \/ intvl (g y) (g x) (g z).
proof: Proof. move=> Hmonot x y z Hx Hy Hz. have Dz: dom z by exact: Hdom Hz. case: Hmonot; rewrite /Rincr /Rdecr =>H; [left|right]; split; apply: H =>//; move: Hz; rewrite /intvl /=; by move=> [H1 H2]. Qed.
imports: Coq(ZArith Psatz Reals) Flocq(Raux) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp Coquelicot Xreal Interval Basic Xreal_derive Interval_compl Datatypes Taylor_poly Basic_rec Bound