--- a/src/HOL/Nat.thy Thu Aug 07 23:56:45 2008 +0200
+++ b/src/HOL/Nat.thy Fri Aug 08 09:26:15 2008 +0200
@@ -1309,9 +1309,24 @@
using `n < n'`
by (induct n n' rule: less_Suc_induct[consumes 1]) (auto intro: mono)
+lemma lift_Suc_mono_less_iff:
+ "(!!n. f n < f(Suc n)) \<Longrightarrow> f(n) < f(m) \<longleftrightarrow> n<m"
+by(blast intro: less_asym' lift_Suc_mono_less[of f]
+ dest: linorder_not_less[THEN iffD1] le_eq_less_or_eq[THEN iffD1])
+
end
+lemma mono_nat_linear_lb:
+ "(!!m n::nat. m<n \<Longrightarrow> f m < f n) \<Longrightarrow> f(m)+k \<le> f(m+k)"
+apply(induct_tac k)
+ apply simp
+apply(erule_tac x="m+n" in meta_allE)
+apply(erule_tac x="m+n+1" in meta_allE)
+apply simp
+done
+
+
text{*Subtraction laws, mostly by Clemens Ballarin*}
lemma diff_less_mono: "[| a < (b::nat); c \<le> a |] ==> a-c < b-c"