1.1 --- a/src/HOL/IntDiv.thy	Wed Jul 25 17:05:50 2007 +0200
     1.2 +++ b/src/HOL/IntDiv.thy	Wed Jul 25 18:10:28 2007 +0200
     1.3 @@ -758,6 +758,15 @@
     1.4  done
     1.5  
     1.6  
     1.7 +lemma zmod_zdiff1_eq: fixes a::int
     1.8 +  shows "(a - b) mod c = (a mod c - b mod c) mod c" (is "?l = ?r")
     1.9 +proof -
    1.10 +  have "?l = (c + (a mod c - b mod c)) mod c"
    1.11 +    using zmod_zadd1_eq[of a "-b" c] by(simp add:ring_simps zmod_zminus1_eq_if)
    1.12 +  also have "\<dots> = ?r" by simp
    1.13 +  finally show ?thesis .
    1.14 +qed
    1.15 +
    1.16  subsection{*Proving  @{term "a div (b*c) = (a div b) div c"} *}
    1.17  
    1.18  (*The condition c>0 seems necessary.  Consider that 7 div ~6 = ~2 but