src/HOL/IntDiv.thy
changeset 24490 a4c2a0ffa5be
parent 24481 c3a4a289decc
child 24630 351a308ab58d
     1.1 --- a/src/HOL/IntDiv.thy	Thu Aug 30 17:09:02 2007 +0200
     1.2 +++ b/src/HOL/IntDiv.thy	Thu Aug 30 21:43:08 2007 +0200
     1.3 @@ -935,6 +935,19 @@
     1.4  apply (auto simp add: mult_commute)
     1.5  done
     1.6  
     1.7 +lemma zmod_zmod_cancel:
     1.8 +assumes "n dvd m" shows "(k::int) mod m mod n = k mod n"
     1.9 +proof -
    1.10 +  from `n dvd m` obtain r where "m = n*r" by(auto simp:dvd_def)
    1.11 +  have "k mod n = (m * (k div m) + k mod m) mod n"
    1.12 +    using zmod_zdiv_equality[of k m] by simp
    1.13 +  also have "\<dots> = (m * (k div m) mod n + k mod m mod n) mod n"
    1.14 +    by(subst zmod_zadd1_eq, rule refl)
    1.15 +  also have "m * (k div m) mod n = 0" using `m = n*r`
    1.16 +    by(simp add:mult_ac)
    1.17 +  finally show ?thesis by simp
    1.18 +qed
    1.19 +
    1.20  
    1.21  subsection {*Splitting Rules for div and mod*}
    1.22