# HG changeset patch
# User huffman
# Date 1231440189 28800
# Node ID f0a8fe83bc07b5c63849be33574afb31e190a051
# Parent  6d10cf26b5dcb507189aa33e65c19d0cc279429c
add lemma dvd_diff to class comm_ring_1

diff -r 6d10cf26b5dc -r f0a8fe83bc07 src/HOL/Ring_and_Field.thy
--- 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