# HG changeset patch
# User nipkow
# Date 1421435199 -3600
# Node ID e7d237c2ce938ad18133ff81b5d301c79392be4c
# Parent  c7f6f01ede154ed513f7170beadabc6a48d15666
added simp lemma

diff -r c7f6f01ede15 -r e7d237c2ce93 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Thu Jan 15 13:39:41 2015 +0100
+++ b/src/HOL/Divides.thy	Fri Jan 16 20:06:39 2015 +0100
@@ -511,6 +511,11 @@
 apply simp
 done
 
+lemma div_minus[simp]:
+  "\<lbrakk> z dvd x; z dvd y\<rbrakk> \<Longrightarrow> (x - y) div z = x div z - y div z"
+using div_add[where y = "- z" for z]
+by (simp add: dvd_neg_div)
+
 lemma div_minus_minus [simp]: "(-a) div (-b) = a div b"
   using div_mult_mult1 [of "- 1" a b]
   unfolding neg_equal_0_iff_equal by simp