--- a/src/HOL/Power.thy Sun Oct 29 19:39:03 2017 +0100
+++ b/src/HOL/Power.thy Mon Oct 30 13:18:41 2017 +0000
@@ -306,6 +306,20 @@
end
+context semidom_divide
+begin
+
+lemma power_diff:
+ "a ^ (m - n) = (a ^ m) div (a ^ n)" if "a \<noteq> 0" and "n \<le> m"
+proof -
+ define q where "q = m - n"
+ with \<open>n \<le> m\<close> have "m = q + n" by simp
+ with \<open>a \<noteq> 0\<close> q_def show ?thesis
+ by (simp add: power_add)
+qed
+
+end
+
context algebraic_semidom
begin
@@ -370,11 +384,6 @@
context field
begin
-lemma power_diff:
- assumes "a \<noteq> 0"
- shows "n \<le> m \<Longrightarrow> a ^ (m - n) = a ^ m / a ^ n"
- by (induct m n rule: diff_induct) (simp_all add: assms power_not_zero)
-
lemma power_divide [field_simps, divide_simps]: "(a / b) ^ n = a ^ n / b ^ n"
by (induct n) simp_all