diff -r ff8386fc191d -r 58191e01f0b1 src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Mon Apr 29 16:50:34 2019 +0100
+++ b/src/HOL/Algebra/Divisibility.thy	Mon Apr 29 17:11:26 2019 +0100
@@ -398,12 +398,12 @@
 
 subsubsection \<open>Multiplication and associativity\<close>
 
-lemma (in monoid_cancel) mult_cong_r:
+lemma (in monoid) mult_cong_r:
   assumes "b \<sim> b'" "a \<in> carrier G"  "b \<in> carrier G"  "b' \<in> carrier G"
   shows "a \<otimes> b \<sim> a \<otimes> b'"
   by (meson assms associated_def divides_mult_lI)
 
-lemma (in comm_monoid_cancel) mult_cong_l:
+lemma (in comm_monoid) mult_cong_l:
   assumes "a \<sim> a'" "a \<in> carrier G"  "a' \<in> carrier G"  "b \<in> carrier G"
   shows "a \<otimes> b \<sim> a' \<otimes> b"
   using assms m_comm mult_cong_r by auto
@@ -723,6 +723,11 @@
   qed
 qed
 
+lemma divides_irreducible_condition:
+  assumes "irreducible G r" and "a \<in> carrier G"
+  shows "a divides\<^bsub>G\<^esub> r \<Longrightarrow> a \<in> Units G \<or> a \<sim>\<^bsub>G\<^esub> r"
+  using assms unfolding irreducible_def properfactor_def associated_def
+  by (cases "r divides\<^bsub>G\<^esub> a", auto)
 
 subsubsection \<open>Prime elements\<close>