diff -r e5cfb05d312e -r 3ae579092045 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sun Sep 11 23:50:36 2022 +0200
+++ b/src/HOL/Divides.thy	Sun Sep 11 16:21:20 2022 +0000
@@ -427,14 +427,6 @@
     by simp
 qed
 
-lemma euclidean_relation_intI' [case_names by0 pos neg]:
-  \<open>(k div l, k mod l) = (q, r)\<close>
-    if \<open>l = 0 \<Longrightarrow> q = 0 \<and> r = k\<close>
-    and \<open>l > 0 \<Longrightarrow> 0 \<le> r \<and> r < l \<and> k = q * l + r\<close>
-    and \<open>l < 0 \<Longrightarrow> l < r \<and> r \<le> 0 \<and> k = q * l + r\<close> for k l q r :: int
-  by (cases l \<open>0::int\<close> rule: linorder_cases)
-    (auto dest: that)
-
 
 subsubsection \<open>Computing \<open>div\<close> and \<open>mod\<close> with shifting\<close>
 
@@ -465,13 +457,21 @@
   if \<open>0 \<le> a\<close> for a b :: int
 proof -
   have \<open>((1 + 2 * b) div (2 * a), (1 + 2 * b) mod (2 * a)) = (b div a, 1 + 2 * (b mod a))\<close>
-  proof (cases \<open>2 * a\<close> \<open>b div a\<close> \<open>1 + 2 * (b mod a)\<close> \<open>1 + 2 * b\<close> rule: euclidean_relation_intI')
+  proof (cases \<open>2 * a\<close> \<open>b div a\<close> \<open>1 + 2 * (b mod a)\<close> \<open>1 + 2 * b\<close> rule: euclidean_relation_intI)
     case by0
     then show ?case
       by simp
   next
-    case pos
-    then have \<open>a > 0\<close>
+    case divides
+    have \<open>even (2 * a)\<close>
+      by simp
+    then have \<open>even (1 + 2 * b)\<close>
+      using \<open>2 * a dvd 1 + 2 * b\<close> by (rule dvd_trans)
+    then show ?case
+      by simp
+  next
+    case euclidean_relation
+    with that have \<open>a > 0\<close>
       by simp
     moreover have \<open>b mod a < a\<close>
       using \<open>a > 0\<close> by simp
@@ -479,12 +479,10 @@
       by simp
     moreover have \<open>2 * (b mod a) + a * (2 * (b div a)) = 2 * (b div a * a + b mod a)\<close>
       by (simp only: algebra_simps)
+    moreover have \<open>0 \<le> 2 * (b mod a)\<close>
+      using \<open>a > 0\<close> by simp
     ultimately show ?case
       by (simp add: algebra_simps)
-  next
-    case neg
-    with that show ?case
-      by simp
   qed
   then show ?Q and ?R
     by simp_all
@@ -495,17 +493,21 @@
   if \<open>a \<le> 0\<close> for a b :: int
 proof -
   have \<open>((1 + 2 * b) div (2 * a), (1 + 2 * b) mod (2 * a)) = ((b + 1) div a, 2 * ((b + 1) mod a) - 1)\<close>
-  proof (cases \<open>2 * a\<close> \<open>(b + 1) div a\<close> \<open>2 * ((b + 1) mod a) - 1\<close> \<open>1 + 2 * b\<close> rule: euclidean_relation_intI')
+  proof (cases \<open>2 * a\<close> \<open>(b + 1) div a\<close> \<open>2 * ((b + 1) mod a) - 1\<close> \<open>1 + 2 * b\<close> rule: euclidean_relation_intI)
     case by0
     then show ?case
       by simp
   next
-    case pos
-    with that show ?case
+    case divides
+    have \<open>even (2 * a)\<close>
+      by simp
+    then have \<open>even (1 + 2 * b)\<close>
+      using \<open>2 * a dvd 1 + 2 * b\<close> by (rule dvd_trans)
+    then show ?case
       by simp
   next
-    case neg
-    then have \<open>a < 0\<close>
+    case euclidean_relation
+    with that have \<open>a < 0\<close>
       by simp
     moreover have \<open>(b + 1) mod a > a\<close>
       using \<open>a < 0\<close> by simp
@@ -519,7 +521,7 @@
       2 * ((1 + b) div a * a + (1 + b) mod a)\<close>
       by (simp only: algebra_simps)
     ultimately show ?case
-      by (simp add: algebra_simps)
+      by (simp add: algebra_simps sgn_mult abs_mult)
   qed
   then show ?Q and ?R
     by simp_all