proposition: Theorem IAF : forall (f:R -> R) (a b k:R) (pr:derivable f), a <= b -> (forall c:R, a <= c <= b -> derive_pt f c (pr c) <= k) -> f b - f a <= k * (b - a).
proof: Proof. intros. destruct (total_order_T a b) as [[H1| -> ]|H1]. - pose proof (MVT_cor1 f _ _ pr H1) as (c & -> & H4). do 2 rewrite <- (Rmult_comm (b - a)). apply Rmult_le_compat_l. + apply Rplus_le_reg_l with a; rewrite Rplus_0_r. replace (a + (b - a)) with b; [ assumption | ring ]. + apply H0. elim H4; intros. split; left; assumption. - unfold Rminus; do 2 rewrite Rplus_opp_r. rewrite Rmult_0_r; right; reflexivity. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H H1)). Qed.
imports: Rbase Rfunctions Ranalysis1 Rtopology Lra