fundamental property of division by units

--- a/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:19 2017 +0200
+++ b/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:19 2017 +0200
@@ -192,6 +192,10 @@
     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