src/HOL/Int.thy
changeset 62128 3201ddb00097
parent 61944 5d06ecfdb472
child 62347 2230b7047376
     1.1 --- a/src/HOL/Int.thy	Mon Jan 11 15:20:17 2016 +0100
     1.2 +++ b/src/HOL/Int.thy	Mon Jan 11 16:38:39 2016 +0100
     1.3 @@ -314,6 +314,12 @@
     1.4    "of_int z < 1 \<longleftrightarrow> z < 1"
     1.5    using of_int_less_iff [of z 1] by simp
     1.6  
     1.7 +lemma of_int_pos: "z > 0 \<Longrightarrow> of_int z > 0"
     1.8 +  by simp
     1.9 +
    1.10 +lemma of_int_nonneg: "z \<ge> 0 \<Longrightarrow> of_int z \<ge> 0"
    1.11 +  by simp
    1.12 +
    1.13  end
    1.14  
    1.15  text \<open>Comparisons involving @{term of_int}.\<close>