src/HOL/Int.thy
changeset 53065 de1816a7293e
parent 52435 6646bb548c6b
child 53652 18fbca265e2e
equal deleted inserted replaced
53064:7e3f39bc41df 53065:de1816a7293e
   382   by transfer clarsimp
   382   by transfer clarsimp
   383 
   383 
   384 lemma nat_zminus_int [simp]: "nat (- int n) = 0"
   384 lemma nat_zminus_int [simp]: "nat (- int n) = 0"
   385   by transfer simp
   385   by transfer simp
   386 
   386 
       
   387 lemma le_nat_iff:
       
   388   "k \<ge> 0 \<Longrightarrow> n \<le> nat k \<longleftrightarrow> int n \<le> k"
       
   389   by transfer auto
       
   390   
   387 lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
   391 lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
   388   by transfer (clarsimp simp add: less_diff_conv)
   392   by transfer (clarsimp simp add: less_diff_conv)
   389 
   393 
   390 context ring_1
   394 context ring_1
   391 begin
   395 begin