# HG changeset patch
# User noschinl
# Date 1371656031 -7200
# Node ID e95f6b4b1bcfd67101090b40d451497a20c73494
# Parent  432777f2e372109bcfcd19c4c30729b21a8178e8
added coprimality lemma

diff -r 432777f2e372 -r e95f6b4b1bcf src/HOL/GCD.thy
--- 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'"