# HG changeset patch
# User haftmann
# Date 1413126335 -7200
# Node ID 1ddba8bcbb58dc3c6a72870140f3fb9e70537b15
# Parent  a62065b5e1e28536686fd49f9dfa4c4adb1229b2
some more facts on divisibility

diff -r a62065b5e1e2 -r 1ddba8bcbb58 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)