changeset 59380 | e7d237c2ce93 |
parent 59058 | a78612c67ec0 |
child 59473 | b0ac740fc510 |
--- 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