src/HOL/Algebra/Multiplicative_Group.thy

   shows "{a[^]x | x. x \<in> (UNIV :: nat set)} = {a[^]x | x. x \<in> {0 .. ord a - 1}}" (is "?L = ?R")
 proof
   show "?R \<subseteq> ?L" by blast
   { fix y assume "y \<in> ?L"
     then obtain x::nat where x:"y = a[^]x" by auto
-    define r where "r = x mod ord a"
-    then obtain q where q:"x = q * ord a + r" using mod_eqD by atomize_elim presburger
+    define r q where "r = x mod ord a" and "q = x div ord a"
+    then have "x = q * ord a + r"
+      by (simp add: div_mult_mod_eq)
     hence "y = (a[^]ord a)[^]q \<otimes> a[^]r"
       using x assms by (simp add: mult.commute nat_pow_mult nat_pow_pow)
     hence "y = a[^]r" using assms by (simp add: pow_ord_eq_1)
     have "r < ord a" using ord_ge_1[OF assms] by (simp add: r_def)
     hence "r \<in> {0 .. ord a - 1}" by (force simp: r_def)

 lemma ord_dvd_pow_eq_1 :
   assumes "finite (carrier G)" "a \<in> carrier G" "a [^] k = \<one>"
   shows "ord a dvd k"
 proof -
   define r where "r = k mod ord a"
-  then obtain q where q:"k = q*ord a + r" using mod_eqD by atomize_elim presburger
+
+  define r q where "r = k mod ord a" and "q = k div ord a"
+  then have q: "k = q * ord a + r"
+    by (simp add: div_mult_mod_eq)
   hence "a[^]k = (a[^]ord a)[^]q \<otimes> a[^]r"
       using assms by (simp add: mult.commute nat_pow_mult nat_pow_pow)
   hence "a[^]k = a[^]r" using assms by (simp add: pow_ord_eq_1)
   hence "a[^]r = \<one>" using assms(3) by simp
   have "r < ord a" using ord_ge_1[OF assms(1-2)] by (simp add: r_def)