src/HOL/Rings.thy

 
 lemma dvd_mod_imp_dvd:
   assumes "c dvd a mod b" and "c dvd b"
   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
 begin