diff -r d2e6a1342c90 -r 02b18f59f903 src/HOL/Library/Code_Target_Nat.thy
--- a/src/HOL/Library/Code_Target_Nat.thy	Sun Aug 21 06:18:23 2022 +0000
+++ b/src/HOL/Library/Code_Target_Nat.thy	Sun Aug 21 06:18:23 2022 +0000
@@ -98,13 +98,13 @@
 begin
 
 lemma divmod_nat_code [code]: \<^marker>\<open>contributor \<open>René Thiemann\<close>\<close> \<^marker>\<open>contributor \<open>Akihisa Yamada\<close>\<close>
-  "Divides.divmod_nat m n = (
+  "Euclidean_Division.divmod_nat m n = (
      let k = integer_of_nat m; l = integer_of_nat n
      in map_prod nat_of_integer nat_of_integer
        (if k = 0 then (0, 0)
         else if l = 0 then (0, k) else
           Code_Numeral.divmod_abs k l))"
-  by (simp add: prod_eq_iff Let_def; transfer)
+  by (simp add: prod_eq_iff Let_def Euclidean_Division.divmod_nat_def; transfer)
     (simp add: nat_div_distrib nat_mod_distrib)
 
 end
@@ -136,15 +136,12 @@
 lemma (in semiring_1) of_nat_code_if:
   "of_nat n = (if n = 0 then 0
      else let
-       (m, q) = Divides.divmod_nat n 2;
+       (m, q) = Euclidean_Division.divmod_nat n 2;
        m' = 2 * of_nat m
      in if q = 0 then m' else m' + 1)"
-proof -
-  from div_mult_mod_eq have *: "of_nat n = of_nat (n div 2 * 2 + n mod 2)" by simp
-  show ?thesis
-    by (simp add: Let_def divmod_nat_def of_nat_add [symmetric])
-      (simp add: * mult.commute of_nat_mult add.commute)
-qed
+  by (cases n)
+    (simp_all add: Let_def Euclidean_Division.divmod_nat_def ac_simps
+      flip: of_nat_numeral of_nat_mult minus_mod_eq_mult_div)
 
 declare of_nat_code_if [code]