--- a/src/HOL/GCD.thy Wed Jun 19 17:16:45 2013 +0200
+++ b/src/HOL/GCD.thy Wed Jun 19 17:33:51 2013 +0200
@@ -714,6 +714,14 @@
coprime_mult_int[of d a b]
by blast
+lemma coprime_power_int:
+ assumes "0 < n" shows "coprime (a :: int) (b ^ n) \<longleftrightarrow> coprime a b"
+ using assms
+proof (induct n)
+ case (Suc n) then show ?case
+ by (cases n) (simp_all add: coprime_mul_eq_int)
+qed simp
+
lemma gcd_coprime_exists_nat:
assumes nz: "gcd (a::nat) b \<noteq> 0"
shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"