src/HOL/Integ/IntDiv.thy

   apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
   apply assumption
   apply (simp add: mult_ac)
   done
 
-lemma zdvd1_eq: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
+lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
 proof
   assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by (simp add: zdvd_abs1)
   hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int)
   hence "nat \<bar>x\<bar> = 1"  by simp
   thus "\<bar>x\<bar> = 1" by (cases "x < 0", auto)