diff -r 17989f6bc7b2 -r 909ba5ed93dd src/HOL/Euclidean_Division.thy
--- a/src/HOL/Euclidean_Division.thy	Mon Oct 09 19:10:49 2017 +0200
+++ b/src/HOL/Euclidean_Division.thy	Mon Oct 09 19:10:51 2017 +0200
@@ -511,7 +511,7 @@
       \<Longrightarrow> euclidean_size (a * b) < euclidean_size (c * b)"
     -- \<open>FIXME justify\<close>
   fixes division_segment :: "'a \<Rightarrow> 'a"
-  assumes is_unit_division_segment: "is_unit (division_segment a)"
+  assumes is_unit_division_segment [simp]: "is_unit (division_segment a)"
     and division_segment_mult:
     "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> division_segment (a * b) = division_segment a * division_segment b"
     and division_segment_mod:
@@ -522,6 +522,10 @@
     \<Longrightarrow> (q * b + r) div b = q"
 begin
 
+lemma division_segment_not_0 [simp]:
+  "division_segment a \<noteq> 0"
+  using is_unit_division_segment [of a] is_unitE [of "division_segment a"] by blast
+
 lemma divmod_cases [case_names divides remainder by0]:
   obtains 
     (divides) q where "b \<noteq> 0"