equal
deleted
inserted
replaced
508 apply (subgoal_tac "y * k = -y * -k") |
508 apply (subgoal_tac "y * k = -y * -k") |
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 |
|
514 lemma div_minus[simp]: |
|
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] |
|
517 by (simp add: dvd_neg_div) |
513 |
518 |
514 lemma div_minus_minus [simp]: "(-a) div (-b) = a div b" |
519 lemma div_minus_minus [simp]: "(-a) div (-b) = a div b" |
515 using div_mult_mult1 [of "- 1" a b] |
520 using div_mult_mult1 [of "- 1" a b] |
516 unfolding neg_equal_0_iff_equal by simp |
521 unfolding neg_equal_0_iff_equal by simp |
517 |
522 |