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