src/HOL/IntDiv.thy
changeset 23401 8c5532263ba9
parent 23365 f31794033ae1
child 23431 25ca91279a9b
     1.1 --- a/src/HOL/IntDiv.thy	Sat Jun 16 15:01:54 2007 +0200
     1.2 +++ b/src/HOL/IntDiv.thy	Sat Jun 16 16:27:35 2007 +0200
     1.3 @@ -834,11 +834,16 @@
     1.4  apply (auto simp add: linorder_neq_iff zdiv_zmult_zmult1_aux1 zdiv_zmult_zmult1_aux2)
     1.5  done
     1.6  
     1.7 +lemma zdiv_zmult_zmult1_if[simp]:
     1.8 +  "(k*m) div (k*n) = (if k = (0::int) then 0 else m div n)"
     1.9 +by (simp add:zdiv_zmult_zmult1)
    1.10 +
    1.11 +(*
    1.12  lemma zdiv_zmult_zmult2: "c \<noteq> (0::int) ==> (a*c) div (b*c) = a div b"
    1.13  apply (drule zdiv_zmult_zmult1)
    1.14  apply (auto simp add: mult_commute)
    1.15  done
    1.16 -
    1.17 +*)
    1.18  
    1.19  
    1.20  subsection{*Distribution of Factors over mod*}