proposition: Theorem derivable_pos_imp_increasing : forall f f' dom, connected dom -> (forall x, dom x -> derivable_pt_lim f x (f' x) /\ (0 <= f' x)%R) -> forall u v, dom u -> dom v -> (u <= v)%R -> (f u <= f v)%R.
proof: Proof. intros f f' dom Hdom Hd u v Hu Hv [Huv|Huv]. assert (forall w, (u <= w <= v)%R -> derivable_pt_lim f w (f' w)). intros w Hw. refine (proj1 (Hd _ _)). exact (Hdom _ _ Hu Hv _ Hw). destruct (MVT_cor2 _ _ _ _ Huv H) as (w, (Hw1, Hw2)). replace (f v) with (f u + (f v - f u))%R by ring. rewrite Hw1. pattern (f u) at 1 ; rewrite <- Rplus_0_r. apply Rplus_le_compat_l. apply Rmult_le_pos. refine (proj2 (Hd _ _)). refine (Hdom _ _ Hu Hv _ _). exact (conj (Rlt_le _ _ (proj1 Hw2)) (Rlt_le _ _ (proj2 Hw2))). rewrite <- (Rplus_opp_r u). unfold Rminus. apply Rplus_le_compat_r. exact (Rlt_le _ _ Huv). rewrite Huv. apply Rle_refl. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Raux)