equal
deleted
inserted
replaced
202 apply (subgoal_tac "m dvd n * ka") |
202 apply (subgoal_tac "m dvd n * ka") |
203 apply (subgoal_tac "m dvd ka") |
203 apply (subgoal_tac "m dvd ka") |
204 apply (case_tac [2] "0 \<le> ka") |
204 apply (case_tac [2] "0 \<le> ka") |
205 apply (metis zdvd_mult_div_cancel dvd_refl dvd_mult_left zmult_commute zrelprime_zdvd_zmult) |
205 apply (metis zdvd_mult_div_cancel dvd_refl dvd_mult_left zmult_commute zrelprime_zdvd_zmult) |
206 apply (metis abs_dvd_iff abs_of_nonneg zadd_0 zgcd_0_left zgcd_commute zgcd_zadd_zmult zgcd_zdvd_zgcd_zmult zgcd_zmult_distrib2_abs zmult_1_right zmult_commute) |
206 apply (metis abs_dvd_iff abs_of_nonneg zadd_0 zgcd_0_left zgcd_commute zgcd_zadd_zmult zgcd_zdvd_zgcd_zmult zgcd_zmult_distrib2_abs zmult_1_right zmult_commute) |
207 apply (metis mult_le_0_iff zdvd_mono zdvd_mult_cancel dvd_triv_left zero_le_mult_iff zle_anti_sym zle_linear zle_refl zmult_commute zrelprime_zdvd_zmult) |
207 apply (metis mult_le_0_iff zdvd_mono zdvd_mult_cancel dvd_triv_left zero_le_mult_iff zle_antisym zle_linear zle_refl zmult_commute zrelprime_zdvd_zmult) |
208 apply (metis dvd_triv_left) |
208 apply (metis dvd_triv_left) |
209 done |
209 done |
210 |
210 |
211 lemma zcong_zless_imp_eq: |
211 lemma zcong_zless_imp_eq: |
212 "0 \<le> a ==> |
212 "0 \<le> a ==> |