src/HOL/Int.thy

--- a/src/HOL/Int.thy	Sun Aug 18 15:29:50 2013 +0200
+++ b/src/HOL/Int.thy	Sun Aug 18 15:29:50 2013 +0200
@@ -384,6 +384,10 @@
 lemma nat_zminus_int [simp]: "nat (- int n) = 0"
   by transfer simp
 
+lemma le_nat_iff:
+  "k \<ge> 0 \<Longrightarrow> n \<le> nat k \<longleftrightarrow> int n \<le> k"
+  by transfer auto
+  
 lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
   by transfer (clarsimp simp add: less_diff_conv)