equal
deleted
inserted
replaced
149 \end{isabelle} |
149 \end{isabelle} |
150 *} |
150 *} |
151 |
151 |
152 |
152 |
153 lemma gcd_dvd_gcd_mult: "gcd m n dvd gcd (k*m) n" |
153 lemma gcd_dvd_gcd_mult: "gcd m n dvd gcd (k*m) n" |
154 apply (blast intro: dvd_trans); |
154 apply (auto intro: dvd_trans [of _ m]) |
155 done |
155 done |
156 |
156 |
157 (*This is half of the proof (by dvd_anti_sym) of*) |
157 (*This is half of the proof (by dvd_anti_sym) of*) |
158 lemma gcd_mult_cancel: "gcd k n = 1 \<Longrightarrow> gcd (k*m) n = gcd m n" |
158 lemma gcd_mult_cancel: "gcd k n = 1 \<Longrightarrow> gcd (k*m) n = gcd m n" |
159 oops |
159 oops |