# HG changeset patch
# User paulson
# Date 1022840844 -7200
# Node ID d5234c261813b29a6884ac06b2adda126e4da9ab
# Parent  e961c197f141439ce1ba22aeca6a36a80a9de1ed
finished an incomplete proof

diff -r e961c197f141 -r d5234c261813 src/HOL/NumberTheory/IntPrimes.thy
--- a/src/HOL/NumberTheory/IntPrimes.thy	Fri May 31 12:22:21 2002 +0200
+++ b/src/HOL/NumberTheory/IntPrimes.thy	Fri May 31 12:27:24 2002 +0200
@@ -663,14 +663,17 @@
 
 lemma "[a = b] (mod m) = (a mod m = b mod m)"
   apply (case_tac "m = 0", simp add: DIVISION_BY_ZERO)
-  apply (case_tac "0 < m")
-   apply (simp add: zcong_zmod_eq)
+  apply (simp add: linorder_neq_iff)
+  apply (erule disjE)  
+   prefer 2 apply (simp add: zcong_zmod_eq)
+  txt{*Remainding case: @{term "m<0"}*}
   apply (rule_tac t = m in zminus_zminus [THEN subst])
   apply (subst zcong_zminus)
   apply (subst zcong_zmod_eq)
    apply arith
-  oops  -- {* FIXME: finish this proof? *}
-
+  apply (frule neg_mod_bound [of _ a], frule neg_mod_bound [of _ b]) 
+  apply (simp add: zmod_zminus2_eq_if)
+  done
 
 subsection {* Modulo *}