equal
deleted
inserted
replaced
1226 done |
1226 done |
1227 |
1227 |
1228 text{*Suggested by Matthias Daum*} |
1228 text{*Suggested by Matthias Daum*} |
1229 lemma int_power_div_base: |
1229 lemma int_power_div_base: |
1230 "\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)" |
1230 "\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)" |
1231 apply (subgoal_tac "k ^ m = k ^ ((m - 1) + 1)") |
1231 apply (subgoal_tac "k ^ m = k ^ ((m - Suc 0) + Suc 0)") |
1232 apply (erule ssubst) |
1232 apply (erule ssubst) |
1233 apply (simp only: power_add) |
1233 apply (simp only: power_add) |
1234 apply simp_all |
1234 apply simp_all |
1235 done |
1235 done |
1236 |
1236 |