src/HOL/NumberTheory/IntPrimes.thy
changeset 13193 d5234c261813
parent 13187 e5434b822a96
child 13517 42efec18f5b2
     1.1 --- a/src/HOL/NumberTheory/IntPrimes.thy	Fri May 31 12:22:21 2002 +0200
     1.2 +++ b/src/HOL/NumberTheory/IntPrimes.thy	Fri May 31 12:27:24 2002 +0200
     1.3 @@ -663,14 +663,17 @@
     1.4  
     1.5  lemma "[a = b] (mod m) = (a mod m = b mod m)"
     1.6    apply (case_tac "m = 0", simp add: DIVISION_BY_ZERO)
     1.7 -  apply (case_tac "0 < m")
     1.8 -   apply (simp add: zcong_zmod_eq)
     1.9 +  apply (simp add: linorder_neq_iff)
    1.10 +  apply (erule disjE)  
    1.11 +   prefer 2 apply (simp add: zcong_zmod_eq)
    1.12 +  txt{*Remainding case: @{term "m<0"}*}
    1.13    apply (rule_tac t = m in zminus_zminus [THEN subst])
    1.14    apply (subst zcong_zminus)
    1.15    apply (subst zcong_zmod_eq)
    1.16     apply arith
    1.17 -  oops  -- {* FIXME: finish this proof? *}
    1.18 -
    1.19 +  apply (frule neg_mod_bound [of _ a], frule neg_mod_bound [of _ b]) 
    1.20 +  apply (simp add: zmod_zminus2_eq_if)
    1.21 +  done
    1.22  
    1.23  subsection {* Modulo *}
    1.24