src/HOL/Divides.thy
changeset 47162 9d7d919b9fd8
parent 47160 8ada79014cb2
child 47163 248376f8881d
     1.1 --- a/src/HOL/Divides.thy	Tue Mar 27 15:34:36 2012 +0200
     1.2 +++ b/src/HOL/Divides.thy	Tue Mar 27 15:40:11 2012 +0200
     1.3 @@ -2207,12 +2207,6 @@
     1.4  lemma abs_div: "(y::int) dvd x \<Longrightarrow> abs (x div y) = abs x div abs y"
     1.5  by (unfold dvd_def, cases "y=0", auto simp add: abs_mult)
     1.6  
     1.7 -lemma zdvd_mult_div_cancel:"(n::int) dvd m \<Longrightarrow> n * (m div n) = m"
     1.8 -apply (subgoal_tac "m mod n = 0")
     1.9 - apply (simp add: zmult_div_cancel)
    1.10 -apply (simp only: dvd_eq_mod_eq_0)
    1.11 -done
    1.12 -
    1.13  text{*Suggested by Matthias Daum*}
    1.14  lemma int_power_div_base:
    1.15       "\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)"