diff -r 96d126844adc -r 65ffe9e910d4 src/HOL/Euclidean_Division.thy
--- a/src/HOL/Euclidean_Division.thy	Sat Feb 01 19:10:37 2020 +0100
+++ b/src/HOL/Euclidean_Division.thy	Sat Feb 01 19:10:40 2020 +0100
@@ -327,6 +327,26 @@
   using div_plus_div_distrib_dvd_left [of c b a]
   by (simp add: ac_simps)
 
+lemma sum_div_partition:
+  \<open>(\<Sum>a\<in>A. f a) div b = (\<Sum>a\<in>A \<inter> {a. b dvd f a}. f a div b) + (\<Sum>a\<in>A \<inter> {a. \<not> b dvd f a}. f a) div b\<close>
+    if \<open>finite A\<close>
+proof -
+  have \<open>A = A \<inter> {a. b dvd f a} \<union> A \<inter> {a. \<not> b dvd f a}\<close>
+    by auto
+  then have \<open>(\<Sum>a\<in>A. f a) = (\<Sum>a\<in>A \<inter> {a. b dvd f a} \<union> A \<inter> {a. \<not> b dvd f a}. f a)\<close>
+    by simp
+  also have \<open>\<dots> = (\<Sum>a\<in>A \<inter> {a. b dvd f a}. f a) + (\<Sum>a\<in>A \<inter> {a. \<not> b dvd f a}. f a)\<close>
+    using \<open>finite A\<close> by (auto intro: sum.union_inter_neutral)
+  finally have *: \<open>sum f A = sum f (A \<inter> {a. b dvd f a}) + sum f (A \<inter> {a. \<not> b dvd f a})\<close> .
+  define B where B: \<open>B = A \<inter> {a. b dvd f a}\<close>
+  with \<open>finite A\<close> have \<open>finite B\<close> and \<open>a \<in> B \<Longrightarrow> b dvd f a\<close> for a
+    by simp_all
+  then have \<open>(\<Sum>a\<in>B. f a) div b = (\<Sum>a\<in>B. f a div b)\<close> and \<open>b dvd (\<Sum>a\<in>B. f a)\<close>
+    by induction (simp_all add: div_plus_div_distrib_dvd_left)
+  then show ?thesis using *
+    by (simp add: B div_plus_div_distrib_dvd_left)
+qed
+
 named_theorems mod_simps
 
 text \<open>Addition respects modular equivalence.\<close>
@@ -442,6 +462,26 @@
     by (simp add: mod_mult_left_eq mod_mult_right_eq)
 qed
 
+lemma power_diff_power_eq:
+  \<open>a ^ m div a ^ n = (if n \<le> m then a ^ (m - n) else 1 div a ^ (n - m))\<close>
+    if \<open>a \<noteq> 0\<close>
+proof (cases \<open>n \<le> m\<close>)
+  case True
+  with that power_diff [symmetric, of a n m] show ?thesis by simp
+next
+  case False
+  then obtain q where n: \<open>n = m + Suc q\<close>
+    by (auto simp add: not_le dest: less_imp_Suc_add)
+  then have \<open>a ^ m div a ^ n = (a ^ m * 1) div (a ^ m * a ^ Suc q)\<close>
+    by (simp add: power_add ac_simps)
+  moreover from that have \<open>a ^ m \<noteq> 0\<close>
+    by simp
+  ultimately have \<open>a ^ m div a ^ n = 1 div a ^ Suc q\<close>
+    by (subst (asm) div_mult_mult1) simp
+  with False n show ?thesis
+    by simp
+qed
+
 end