src/HOL/IntDiv.thy
changeset 30079 293b896b9c25
parent 30042 31039ee583fa
child 30180 6d29a873141f
     1.1 --- a/src/HOL/IntDiv.thy	Mon Feb 23 13:55:36 2009 -0800
     1.2 +++ b/src/HOL/IntDiv.thy	Mon Feb 23 16:25:52 2009 -0800
     1.3 @@ -1228,7 +1228,7 @@
     1.4  text{*Suggested by Matthias Daum*}
     1.5  lemma int_power_div_base:
     1.6       "\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)"
     1.7 -apply (subgoal_tac "k ^ m = k ^ ((m - 1) + 1)")
     1.8 +apply (subgoal_tac "k ^ m = k ^ ((m - Suc 0) + Suc 0)")
     1.9   apply (erule ssubst)
    1.10   apply (simp only: power_add)
    1.11   apply simp_all