equal
deleted
inserted
replaced
192 apply (cases "a = 0") |
192 apply (cases "a = 0") |
193 apply simp |
193 apply simp |
194 apply (unfold dvd_def) |
194 apply (unfold dvd_def) |
195 apply auto |
195 apply auto |
196 apply(blast intro:mult_assoc[symmetric]) |
196 apply(blast intro:mult_assoc[symmetric]) |
197 apply(fastsimp simp add: mult_assoc) |
197 apply(fastforce simp add: mult_assoc) |
198 done |
198 done |
199 |
199 |
200 lemma dvd_mod_imp_dvd: "[| k dvd m mod n; k dvd n |] ==> k dvd m" |
200 lemma dvd_mod_imp_dvd: "[| k dvd m mod n; k dvd n |] ==> k dvd m" |
201 apply (subgoal_tac "k dvd (m div n) *n + m mod n") |
201 apply (subgoal_tac "k dvd (m div n) *n + m mod n") |
202 apply (simp add: mod_div_equality) |
202 apply (simp add: mod_div_equality) |
2230 done |
2230 done |
2231 |
2231 |
2232 |
2232 |
2233 lemma zmod_le_nonneg_dividend: "(m::int) \<ge> 0 ==> m mod k \<le> m" |
2233 lemma zmod_le_nonneg_dividend: "(m::int) \<ge> 0 ==> m mod k \<le> m" |
2234 apply (rule split_zmod[THEN iffD2]) |
2234 apply (rule split_zmod[THEN iffD2]) |
2235 apply(fastsimp dest: q_pos_lemma intro: split_mult_pos_le) |
2235 apply(fastforce dest: q_pos_lemma intro: split_mult_pos_le) |
2236 done |
2236 done |
2237 |
2237 |
2238 |
2238 |
2239 subsubsection {* The Divides Relation *} |
2239 subsubsection {* The Divides Relation *} |
2240 |
2240 |