| changeset 29879 | 4425849f5db7 |
| parent 29854 | 708c1c7c87ec |
| child 30056 | 0a35bee25c20 |
| child 30240 | 5b25fee0362c |
--- a/src/HOL/Nat.thy Wed Feb 11 11:22:42 2009 -0800 +++ b/src/HOL/Nat.thy Thu Feb 12 18:14:43 2009 +0100 @@ -1367,6 +1367,9 @@ end +lemma mono_iff_le_Suc: "mono f = (\<forall>n. f n \<le> f (Suc n))" +unfolding mono_def +by (auto intro:lift_Suc_mono_le[of f]) lemma mono_nat_linear_lb: "(!!m n::nat. m<n \<Longrightarrow> f m < f n) \<Longrightarrow> f(m)+k \<le> f(m+k)"