diff -r 19837257fd89 -r e7497a1de8b9 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Tue Sep 13 18:56:48 2022 +0100
+++ b/src/HOL/Divides.thy	Tue Sep 13 12:30:37 2022 +0000
@@ -262,8 +262,8 @@
       \<open>a mod b = r\<close> (is ?R)
 proof -
   from assms have \<open>(a div b, a mod b) = (q, r)\<close>
-    by (cases b q r a rule: euclidean_relationI)
-      (auto simp add: division_segment_int_def ac_simps dvd_add_left_iff dest: zdvd_imp_le)
+    by (cases b q r a rule: euclidean_relation_intI)
+      (auto simp add: ac_simps dvd_add_left_iff sgn_1_pos le_less dest: zdvd_imp_le)
   then show ?Q and ?R
     by simp_all
 qed
@@ -400,34 +400,6 @@
 qed
 
 
-subsubsection \<open>Uniqueness rules\<close>
-
-lemma euclidean_relation_intI [case_names by0 divides euclidean_relation]:
-  \<open>(k div l, k mod l) = (q, r)\<close>
-    if by0': \<open>l = 0 \<Longrightarrow> q = 0 \<and> r = k\<close>
-    and divides': \<open>l \<noteq> 0 \<Longrightarrow> l dvd k \<Longrightarrow> r = 0 \<and> k = q * l\<close>
-    and euclidean_relation': \<open>l \<noteq> 0 \<Longrightarrow> \<not> l dvd k \<Longrightarrow> sgn r = sgn l
-      \<and> \<bar>r\<bar> < \<bar>l\<bar> \<and> k = q * l + r\<close> for k l :: int
-proof (cases l q r k rule: euclidean_relationI)
-  case by0
-  then show ?case
-    by (rule by0')
-next
-  case divides
-  then show ?case
-    by (rule divides')
-next
-  case euclidean_relation
-  with euclidean_relation' have \<open>sgn r = sgn l\<close> \<open>\<bar>r\<bar> < \<bar>l\<bar>\<close> \<open>k = q * l + r\<close>
-    by simp_all
-  from \<open>sgn r = sgn l\<close> \<open>l \<noteq> 0\<close> have \<open>division_segment r = division_segment l\<close>
-    by (simp add: division_segment_int_def sgn_if split: if_splits)
-  with \<open>\<bar>r\<bar> < \<bar>l\<bar>\<close> \<open>k = q * l + r\<close>
-  show ?case
-    by simp
-qed
-
-
 subsubsection \<open>Computing \<open>div\<close> and \<open>mod\<close> with shifting\<close>
 
 lemma div_pos_geq: