src/HOL/Ring_and_Field.thy

--- a/src/HOL/Ring_and_Field.thy	Fri Nov 13 19:49:13 2009 +0100
+++ b/src/HOL/Ring_and_Field.thy	Fri Nov 13 22:01:01 2009 +0100
@@ -1301,6 +1301,10 @@
 lemma dvd_abs_iff [simp]: "m dvd (abs k) \<longleftrightarrow> m dvd k"
   by (simp add: abs_if)
 
+lemma dvd_if_abs_eq:
+  "abs l = abs (k) \<Longrightarrow> l dvd k"
+by(subst abs_dvd_iff[symmetric]) simp
+
 end
 
 class ordered_field = field + ordered_idom