equal
deleted
inserted
replaced
542 prefer 2 |
542 prefer 2 |
543 apply (rule_tac n = n in zrelprime_zdvd_zmult) |
543 apply (rule_tac n = n in zrelprime_zdvd_zmult) |
544 apply (simp add: zgcd_commute) |
544 apply (simp add: zgcd_commute) |
545 apply (simp add: zmult_commute) |
545 apply (simp add: zmult_commute) |
546 apply (auto simp add: dvd_def) |
546 apply (auto simp add: dvd_def) |
547 apply (blast intro: sym) |
|
548 done |
547 done |
549 |
548 |
550 lemma zcong_zless_imp_eq: |
549 lemma zcong_zless_imp_eq: |
551 "0 \<le> a ==> |
550 "0 \<le> a ==> |
552 a < m ==> 0 \<le> b ==> b < m ==> [a = b] (mod m) ==> a = b" |
551 a < m ==> 0 \<le> b ==> b < m ==> [a = b] (mod m) ==> a = b" |