diff -r ddf255a4ccc3 -r 5e6b195eee83 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Thu Nov 09 15:11:51 2023 +0000
+++ b/src/HOL/Code_Numeral.thy	Thu Nov 09 15:11:52 2023 +0000
@@ -305,7 +305,7 @@
   "division_segment (k :: integer) = (if k \<ge> 0 then 1 else - 1)"
   by transfer (simp add: division_segment_int_def)
 
-instance integer :: unique_euclidean_ring_with_nat
+instance integer :: linordered_euclidean_semiring
   by (standard; transfer) (simp_all add: of_nat_div division_segment_int_def)
 
 instantiation integer :: ring_bit_operations
@@ -393,7 +393,7 @@
 
 end
 
-instantiation integer :: unique_euclidean_semiring_with_nat_division
+instantiation integer :: linordered_euclidean_semiring_division
 begin
 
 definition divmod_integer :: "num \<Rightarrow> num \<Rightarrow> integer \<times> integer"
@@ -1065,9 +1065,9 @@
   by (simp add: natural_eq_iff)
 
 instance natural :: discrete_linordered_semidom
-  by (standard; transfer) simp_all
+  by (standard; transfer) (simp_all add: Suc_le_eq)
 
-instance natural :: unique_euclidean_semiring_with_nat
+instance natural :: linordered_euclidean_semiring
   by (standard; transfer) simp_all
 
 instantiation natural :: semiring_bit_operations