equal
deleted
inserted
replaced
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) |
97 apply (blast intro: zdvd_trans) |
97 apply (blast intro: zdvd_trans dvd_triv_right) |
98 done |
98 done |
99 |
99 |
100 lemma zgcd_zmult_zdvd_zgcd: |
100 lemma zgcd_zmult_zdvd_zgcd: |
101 "zgcd k n = 1 ==> zgcd (k * m) n dvd zgcd m n" |
101 "zgcd k n = 1 ==> zgcd (k * m) n dvd zgcd m n" |
102 apply (simp add: zgcd_greatest_iff) |
102 apply (simp add: zgcd_greatest_iff) |