src/HOL/Euclidean_Division.thy

--- a/src/HOL/Euclidean_Division.thy	Mon Oct 09 19:10:47 2017 +0200
+++ b/src/HOL/Euclidean_Division.thy	Mon Oct 09 19:10:48 2017 +0200
@@ -488,6 +488,18 @@
   then show ?P by simp
 qed
 
+lemma mod_eqE:
+  assumes "a mod c = b mod c"
+  obtains d where "b = a + c * d"
+proof -
+  from assms have "c dvd a - b"
+    by (simp add: mod_eq_dvd_iff)
+  then obtain d where "a - b = c * d" ..
+  then have "b = a + c * - d"
+    by (simp add: algebra_simps)
+  with that show thesis .
+qed
+
 end