src/HOL/Euclidean_Division.thy

   hence z: "b = c * a" by (simp add: mult.commute)
   from z assms have "\<not>is_unit c" by (auto simp: mult.commute mult_unit_dvd_iff)
   with z assms show ?thesis
     by (auto intro!: euclidean_size_times_nonunit)
 qed
+
+lemma unit_imp_mod_eq_0:
+  "a mod b = 0" if "is_unit b"
+  using that by (simp add: mod_eq_0_iff_dvd unit_imp_dvd)
 
 end
 
 class euclidean_ring = idom_modulo + euclidean_semiring