# HG changeset patch
# User paulson
# Date 1186571671 -7200
# Node ID 102ebceaa495c513227885e7787dcf1ee0bbef61
# Parent  9f818139951be2a62bd68da2e8ec5ec35648198f
metis

diff -r 9f818139951b -r 102ebceaa495 src/HOL/NumberTheory/IntPrimes.thy
--- a/src/HOL/NumberTheory/IntPrimes.thy	Tue Aug 07 23:24:10 2007 +0200
+++ b/src/HOL/NumberTheory/IntPrimes.thy	Wed Aug 08 13:14:31 2007 +0200
@@ -140,10 +140,7 @@
 
 lemma zrelprime_zdvd_zmult_aux:
      "zgcd (n, k) = 1 ==> k dvd m * n ==> 0 \<le> m ==> k dvd m"
-  apply (subgoal_tac "m = zgcd (m * n, m * k)")
-   apply (erule ssubst, rule zgcd_greatest_iff [THEN iffD2])
-   apply (simp_all add: zgcd_zmult_distrib2 [symmetric] zero_le_mult_iff)
-  done
+  by (metis abs_of_nonneg zdvd_triv_right zgcd_greatest_iff zgcd_zmult_distrib2_abs zmult_1_right)
 
 lemma zrelprime_zdvd_zmult: "zgcd (n, k) = 1 ==> k dvd m * n ==> k dvd m"
   apply (case_tac "0 \<le> m")
@@ -247,7 +244,6 @@
 
 lemma zcong_zmult:
     "[a = b] (mod m) ==> [c = d] (mod m) ==> [a * c = b * d] (mod m)"
-
   apply (rule_tac b = "b * c" in zcong_trans)
    apply (unfold zcong_def)
   apply (metis zdiff_zmult_distrib2 zdvd_zmult zmult_commute)