some more facts on divisibility
authorhaftmann
Sun, 12 Oct 2014 17:05:35 +0200
changeset 58650 1ddba8bcbb58
parent 58649 a62065b5e1e2
child 58651 cfdd09041638
some more facts on divisibility
src/HOL/Int.thy
--- a/src/HOL/Int.thy	Sun Oct 12 17:05:34 2014 +0200
+++ b/src/HOL/Int.thy	Sun Oct 12 17:05:35 2014 +0200
@@ -1333,6 +1333,10 @@
 lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
   unfolding zdvd_int by (cases "z \<ge> 0") simp_all
 
+lemma dvd_int_unfold_dvd_nat:
+  "k dvd l \<longleftrightarrow> nat \<bar>k\<bar> dvd nat \<bar>l\<bar>"
+  unfolding dvd_int_iff [symmetric] by simp
+
 lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
   by (auto simp add: dvd_int_iff)