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