equal
deleted
inserted
replaced
329 apply (frule given_quot) |
329 apply (frule given_quot) |
330 apply (rule trans) |
330 apply (rule trans) |
331 prefer 2 |
331 prefer 2 |
332 apply (erule asm_rl) |
332 apply (erule asm_rl) |
333 apply (rule_tac f="%n. n div f" in arg_cong) |
333 apply (rule_tac f="%n. n div f" in arg_cong) |
334 apply (simp add : mult_ac) |
334 apply (simp add : ac_simps) |
335 done |
335 done |
336 |
336 |
337 lemma diff_mod_le: "(a::nat) < d ==> b dvd d ==> a - a mod b <= d - b" |
337 lemma diff_mod_le: "(a::nat) < d ==> b dvd d ==> a - a mod b <= d - b" |
338 apply (unfold dvd_def) |
338 apply (unfold dvd_def) |
339 apply clarify |
339 apply clarify |