# HG changeset patch
# User haftmann
# Date 1507494499 -7200
# Node ID 39bb2462e681216b98edba7279baafc4aad7f90e
# Parent  9c9baae292177f2a24feaa815bc20575821842b7
fundamental property of division by units

diff -r 9c9baae29217 -r 39bb2462e681 src/HOL/Euclidean_Division.thy
--- 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