--- a/src/HOL/Limits.thy Wed Apr 02 16:34:37 2014 +0100
+++ b/src/HOL/Limits.thy Wed Apr 02 16:45:31 2014 +0100
@@ -404,6 +404,10 @@
lemma tendsto_Zfun_iff: "(f ---> a) F = Zfun (\<lambda>x. f x - a) F"
by (simp only: tendsto_iff Zfun_def dist_norm)
+lemma tendsto_0_le: "\<lbrakk>(f ---> 0) F; eventually (\<lambda>x. norm (g x) \<le> norm (f x) * K) F\<rbrakk>
+ \<Longrightarrow> (g ---> 0) F"
+ by (simp add: Zfun_imp_Zfun tendsto_Zfun_iff)
+
subsubsection {* Distance and norms *}
lemma tendsto_dist [tendsto_intros]: