# HG changeset patch
# User nipkow
# Date 1259913129 -3600
# Node ID fcc20072df9aaab66629aefbd20a67c1c7755b1b
# Parent  8493ed132fed5d3443d9b74c65e0fd0efb4ede91
removed redundant lemma

diff -r 8493ed132fed -r fcc20072df9a src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Fri Dec 04 08:26:25 2009 +0100
+++ b/src/HOL/GCD.thy	Fri Dec 04 08:52:09 2009 +0100
@@ -779,14 +779,6 @@
   apply auto
 done
 
-lemma coprime_divprod_nat: "(d::nat) dvd a * b  \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b"
-  using coprime_dvd_mult_iff_nat[of d a b]
-  by (auto simp add: mult_commute)
-
-lemma coprime_divprod_int: "(d::int) dvd a * b  \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b"
-  using coprime_dvd_mult_iff_int[of d a b]
-  by (auto simp add: mult_commute)
-
 lemma division_decomp_nat: assumes dc: "(a::nat) dvd b * c"
   shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
 proof-
diff -r 8493ed132fed -r fcc20072df9a src/HOL/Number_Theory/Primes.thy
--- a/src/HOL/Number_Theory/Primes.thy	Fri Dec 04 08:26:25 2009 +0100
+++ b/src/HOL/Number_Theory/Primes.thy	Fri Dec 04 08:52:09 2009 +0100
@@ -360,16 +360,15 @@
     from prime_dvd_mult_nat[OF p pab']
     have "p dvd a \<or> p dvd b" .
     moreover
-    {assume pa: "p dvd a"
-      have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
+    { assume pa: "p dvd a"
       from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto
       with p have "coprime b p"
         by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
       hence pnb: "coprime (p^n) b"
         by (subst gcd_commute_nat, rule coprime_exp_nat)
-      from coprime_divprod_nat[OF pnba pnb] have ?thesis by blast }
+      from coprime_dvd_mult_nat[OF pnb pab] have ?thesis by blast }
     moreover
-    {assume pb: "p dvd b"
+    { assume pb: "p dvd b"
       have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
       from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a"
         by auto
@@ -377,7 +376,7 @@
         by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
       hence pna: "coprime (p^n) a"
         by (subst gcd_commute_nat, rule coprime_exp_nat)
-      from coprime_divprod_nat[OF pab pna] have ?thesis by blast }
+      from coprime_dvd_mult_nat[OF pna pnba] have ?thesis by blast }
     ultimately have ?thesis by blast}
   ultimately show ?thesis by blast
 qed