equal
deleted
inserted
replaced
86 "0 \<le> (m::int) ==> zprime p ==> p dvd m * n ==> p dvd m \<or> p dvd n" |
86 "0 \<le> (m::int) ==> zprime p ==> p dvd m * n ==> p dvd m \<or> p dvd n" |
87 by (metis zgcd_zdvd1 zgcd_zdvd2 zgcd_pos zprime_def zrelprime_dvd_mult) |
87 by (metis zgcd_zdvd1 zgcd_zdvd2 zgcd_pos zprime_def zrelprime_dvd_mult) |
88 |
88 |
89 lemma zgcd_zadd_zmult [simp]: "zgcd (m + n * k) n = zgcd m n" |
89 lemma zgcd_zadd_zmult [simp]: "zgcd (m + n * k) n = zgcd m n" |
90 apply (rule zgcd_eq [THEN trans]) |
90 apply (rule zgcd_eq [THEN trans]) |
91 apply (simp add: zmod_zadd1_eq) |
91 apply (simp add: mod_add_eq) |
92 apply (rule zgcd_eq [symmetric]) |
92 apply (rule zgcd_eq [symmetric]) |
93 done |
93 done |
94 |
94 |
95 lemma zgcd_zdvd_zgcd_zmult: "zgcd m n dvd zgcd (k * m) n" |
95 lemma zgcd_zdvd_zgcd_zmult: "zgcd m n dvd zgcd (k * m) n" |
96 apply (simp add: zgcd_greatest_iff) |
96 apply (simp add: zgcd_greatest_iff) |