proposition: Lemma Rderive_cst_sign (f f' : R -> R) : connected P -> Rderive_over f f' -> Rcst_sign f' -> Rmonot f.
proof: Proof. move=> Hco Hder [H|H]. left; exact: Rderive_pos_imp_incr H. right; exact: Rderive_neg_imp_decr H. Qed.
imports: Coq(ZArith Reals Psatz) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat bigop) Coquelicot(Coquelicot) Stdlib MathComp Xreal Interval Taylor