src/HOL/Rings.thy

--- a/src/HOL/Rings.thy	Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Rings.thy	Sun Oct 08 22:28:21 2017 +0200
@@ -1620,6 +1620,10 @@
   shows "c dvd a"
   using assms dvd_mod_iff [of c b a] by simp
 
+lemma dvd_minus_mod [simp]:
+  "b dvd a - a mod b"
+  by (simp add: minus_mod_eq_div_mult)
+
 end
 
 class idom_modulo = idom + semidom_modulo