# HG changeset patch
# User haftmann
# Date 1376832590 -7200
# Node ID de1816a7293eb1610777de6410d91f5723eeb5c6
# Parent  7e3f39bc41dfad113557c81aa007d8b9f1987dac
added lemma

diff -r 7e3f39bc41df -r de1816a7293e 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)