src/HOL/IntDiv.thy
changeset 30180 6d29a873141f
parent 30079 293b896b9c25
child 30181 05629f28f0f7
     1.1 --- a/src/HOL/IntDiv.thy	Sat Feb 28 21:34:33 2009 +0100
     1.2 +++ b/src/HOL/IntDiv.thy	Sun Mar 01 10:24:57 2009 +0100
     1.3 @@ -1225,6 +1225,9 @@
     1.4  apply (auto simp add: IntDiv.divmod_rel_def of_nat_mult)
     1.5  done
     1.6  
     1.7 +lemma abs_div: "(y::int) dvd x \<Longrightarrow> abs (x div y) = abs x div abs y"
     1.8 +by (unfold dvd_def, cases "y=0", auto simp add: abs_mult)
     1.9 +
    1.10  text{*Suggested by Matthias Daum*}
    1.11  lemma int_power_div_base:
    1.12       "\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)"