diff -r a0ab0dc28d3c -r 3c587b7c3d5c src/HOL/Euclidean_Division.thy
--- a/src/HOL/Euclidean_Division.thy	Tue Oct 26 16:22:03 2021 +0100
+++ b/src/HOL/Euclidean_Division.thy	Tue Oct 26 14:43:59 2021 +0000
@@ -2110,6 +2110,30 @@
 instance int :: unique_euclidean_ring_with_nat
   by standard (simp_all add: dvd_eq_mod_eq_0 divide_int_def division_segment_int_def)
 
+lemma zdiv_zmult2_eq:
+  \<open>a div (b * c) = (a div b) div c\<close> if \<open>c \<ge> 0\<close> for a b c :: int
+proof (cases \<open>b \<ge> 0\<close>)
+  case True
+  with that show ?thesis
+    using div_mult2_eq' [of a \<open>nat b\<close> \<open>nat c\<close>] by simp
+next
+  case False
+  with that show ?thesis
+    using div_mult2_eq' [of \<open>- a\<close> \<open>nat (- b)\<close> \<open>nat c\<close>] by simp
+qed
+
+lemma zmod_zmult2_eq:
+  \<open>a mod (b * c) = b * (a div b mod c) + a mod b\<close> if \<open>c \<ge> 0\<close> for a b c :: int
+proof (cases \<open>b \<ge> 0\<close>)
+  case True
+  with that show ?thesis
+    using mod_mult2_eq' [of a \<open>nat b\<close> \<open>nat c\<close>] by simp
+next
+  case False
+  with that show ?thesis
+    using mod_mult2_eq' [of \<open>- a\<close> \<open>nat (- b)\<close> \<open>nat c\<close>] by simp
+qed
+
 
 subsection \<open>Code generation\<close>