src/HOL/Power.thy
 changeset 66936 cf8d8fc23891 parent 66912 a99a7cbf0fb5 child 67226 ec32cdaab97b
```     1.1 --- a/src/HOL/Power.thy	Sun Oct 29 19:39:03 2017 +0100
1.2 +++ b/src/HOL/Power.thy	Mon Oct 30 13:18:41 2017 +0000
1.3 @@ -306,6 +306,20 @@
1.4
1.5  end
1.6
1.7 +context semidom_divide
1.8 +begin
1.9 +
1.10 +lemma power_diff:
1.11 +  "a ^ (m - n) = (a ^ m) div (a ^ n)" if "a \<noteq> 0" and "n \<le> m"
1.12 +proof -
1.13 +  define q where "q = m - n"
1.14 +  with \<open>n \<le> m\<close> have "m = q + n" by simp
1.15 +  with \<open>a \<noteq> 0\<close> q_def show ?thesis
1.17 +qed
1.18 +
1.19 +end
1.20 +
1.21  context algebraic_semidom
1.22  begin
1.23
1.24 @@ -370,11 +384,6 @@
1.25  context field
1.26  begin
1.27
1.28 -lemma power_diff:
1.29 -  assumes "a \<noteq> 0"
1.30 -  shows "n \<le> m \<Longrightarrow> a ^ (m - n) = a ^ m / a ^ n"
1.31 -  by (induct m n rule: diff_induct) (simp_all add: assms power_not_zero)
1.32 -
1.33  lemma power_divide [field_simps, divide_simps]: "(a / b) ^ n = a ^ n / b ^ n"
1.34    by (induct n) simp_all
1.35
```