add lemma dvd_diff to class comm_ring_1

--- a/src/HOL/Ring_and_Field.thy	Thu Jan 08 10:26:50 2009 -0800
+++ b/src/HOL/Ring_and_Field.thy	Thu Jan 08 10:43:09 2009 -0800
@@ -319,6 +319,9 @@
   then show "- x dvd y" ..
 qed
 
+lemma dvd_diff: "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"
+  by (simp add: diff_minus dvd_add dvd_minus_iff)
+
 end
 
 class ring_no_zero_divisors = ring + no_zero_divisors