diff -r bf1bdf335ea0 -r d8d2a2b97168 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Wed Mar 26 09:19:04 2014 +0100
+++ b/src/HOL/Deriv.thy	Wed Mar 26 14:00:37 2014 +0000
@@ -1364,6 +1364,33 @@
     by simp
 qed
 
+lemma DERIV_pos_imp_increasing_at_bot:
+  fixes f :: "real => real"
+  assumes "\<And>x. x \<le> b \<Longrightarrow> (EX y. DERIV f x :> y & y > 0)"
+      and lim: "(f ---> flim) at_bot"
+  shows "flim < f b"
+proof -
+  have "flim \<le> f (b - 1)"
+    apply (rule tendsto_ge_const [OF _ lim])
+    apply (auto simp: trivial_limit_at_bot_linorder eventually_at_bot_linorder)
+    apply (rule_tac x="b - 2" in exI)
+    apply (force intro: order.strict_implies_order DERIV_pos_imp_increasing [where f=f] assms)
+    done
+  also have "... < f b"
+    by (force intro: DERIV_pos_imp_increasing [where f=f] assms)
+  finally show ?thesis .
+qed
+
+lemma DERIV_neg_imp_decreasing_at_top:
+  fixes f :: "real => real"
+  assumes der: "\<And>x. x \<ge> b \<Longrightarrow> (EX y. DERIV f x :> y & y < 0)"
+      and lim: "(f ---> flim) at_top"
+  shows "flim < f b"
+  apply (rule DERIV_pos_imp_increasing_at_bot [where f = "\<lambda>i. f (-i)" and b = "-b", simplified])
+  apply (metis DERIV_mirror der le_minus_iff neg_0_less_iff_less)
+  apply (metis filterlim_at_top_mirror lim)
+  done
+
 text {* Derivative of inverse function *}
 
 lemma DERIV_inverse_function: