proposition: Lemma Rderive_pos_imp_incr (f f' : R -> R) : connected P -> Rderive_over f f' -> Rpos_over f' -> Rincr f.
proof: Proof. rewrite /Rpos_over /Rincr. move=> Hco Hder H0 x y Hx Hy Hxy; rewrite //=. eapply (derivable_pos_imp_increasing f f' P) =>//. move=> r Hr. move/(_ _ Hr) in Hder. move/(_ _ Hr) in H0. apply: conj H0. exact/is_derive_Reals. Qed.
imports: Coq(ZArith Reals Psatz) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat bigop) Coquelicot(Coquelicot) Stdlib MathComp Xreal Interval Taylor