diff -r 77a96ed74340 -r 9469d9223689 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Tue Dec 21 22:11:10 2021 +0100
+++ b/src/HOL/GCD.thy	Sun Dec 26 11:01:27 2021 +0000
@@ -1637,6 +1637,26 @@
 
 end
 
+text \<open>And some consequences: cancellation modulo @{term m}\<close>
+lemma mult_mod_cancel_right:
+  fixes m :: "'a::{euclidean_ring_cancel,semiring_gcd}"
+  assumes eq: "(a * n) mod m = (b * n) mod m" and "coprime m n" 
+  shows "a mod m = b mod m"
+proof -
+  have "m dvd (a*n - b*n)" 
+    using eq mod_eq_dvd_iff by blast
+  then have "m dvd a-b"
+    by (metis \<open>coprime m n\<close> coprime_dvd_mult_left_iff left_diff_distrib')
+  then show ?thesis
+    using mod_eq_dvd_iff by blast
+qed
+
+lemma mult_mod_cancel_left:
+  fixes m :: "'a::{euclidean_ring_cancel,semiring_gcd}"
+  assumes "(n * a) mod m = (n * b) mod m" and "coprime m n" 
+  shows "a mod m = b mod m"
+  by (metis assms mult.commute mult_mod_cancel_right)
+
 
 subsection \<open>GCD and LCM for multiplicative normalisation functions\<close>