src/HOL/Int.thy
changeset 56889 48a745e1bde7
parent 56525 b5b6ad5dc2ae
child 57512 cc97b347b301
--- a/src/HOL/Int.thy	Tue May 06 23:35:24 2014 +0200
+++ b/src/HOL/Int.thy	Wed May 07 12:25:35 2014 +0200
@@ -293,6 +293,10 @@
 
 end
 
+lemma of_nat_less_of_int_iff:
+  "(of_nat n::'a::linordered_idom) < of_int x \<longleftrightarrow> int n < x"
+  by (metis of_int_of_nat_eq of_int_less_iff)
+
 lemma of_int_eq_id [simp]: "of_int = id"
 proof
   fix z show "of_int z = id z"