equal
deleted
inserted
replaced
509 apply (erule ssubst, rule div_mult_self1_is_id) |
509 apply (erule ssubst, rule div_mult_self1_is_id) |
510 apply simp |
510 apply simp |
511 apply simp |
511 apply simp |
512 done |
512 done |
513 |
513 |
514 lemma div_minus[simp]: |
514 lemma div_diff[simp]: |
515 "\<lbrakk> z dvd x; z dvd y\<rbrakk> \<Longrightarrow> (x - y) div z = x div z - y div z" |
515 "\<lbrakk> z dvd x; z dvd y\<rbrakk> \<Longrightarrow> (x - y) div z = x div z - y div z" |
516 using div_add[where y = "- z" for z] |
516 using div_add[where y = "- z" for z] |
517 by (simp add: dvd_neg_div) |
517 by (simp add: dvd_neg_div) |
518 |
518 |
519 lemma div_minus_minus [simp]: "(-a) div (-b) = a div b" |
519 lemma div_minus_minus [simp]: "(-a) div (-b) = a div b" |