# HG changeset patch # User boehmes # Date 1421447069 -3600 # Node ID a78e71fcd1465e89334454affd75bbf2a64de76e # Parent de4218223e009c4c18d0b0e52220c753576a7d98# Parent e7d237c2ce938ad18133ff81b5d301c79392be4c merged diff -r de4218223e00 -r a78e71fcd146 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Fri Jan 16 23:23:31 2015 +0100 +++ b/src/HOL/Divides.thy Fri Jan 16 23:24:29 2015 +0100 @@ -511,6 +511,11 @@ apply simp done +lemma div_minus[simp]: + "\ z dvd x; z dvd y\ \ (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