# HG changeset patch
# User haftmann
# Date 1571476537 0
# Node ID cb161182ce7f6c30bcaa6ce341e26d0be86bb4eb
# Parent  94a0c47b8553a9b9ba7e1df56dfce16ec5ab4d76
generalized

diff -r 94a0c47b8553 -r cb161182ce7f src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Fri Oct 18 18:41:33 2019 +0000
+++ b/src/HOL/Rings.thy	Sat Oct 19 09:15:37 2019 +0000
@@ -1684,6 +1684,15 @@
 lemma minus_mod_eq_mult_div: "a - a mod b = b * (a div b)"
   by (rule add_implies_diff [symmetric]) (fact mult_div_mod_eq)
 
+lemma mod_0_imp_dvd [dest!]:
+  "b dvd a" if "a mod b = 0"
+proof -
+  have "b dvd (a div b) * b" by simp
+  also have "(a div b) * b = a"
+    using div_mult_mod_eq [of a b] by (simp add: that)
+  finally show ?thesis .
+qed
+
 lemma [nitpick_unfold]:
   "a mod b = a - a div b * b"
   by (fact minus_div_mult_eq_mod [symmetric])
@@ -1718,15 +1727,6 @@
   "b mod a = 0" if "a dvd b"
   using that minus_div_mult_eq_mod [of b a] by simp
 
-lemma mod_0_imp_dvd [dest!]: 
-  "b dvd a" if "a mod b = 0"
-proof -
-  have "b dvd (a div b) * b" by simp
-  also have "(a div b) * b = a"
-    using div_mult_mod_eq [of a b] by (simp add: that)
-  finally show ?thesis .
-qed
-
 lemma mod_eq_0_iff_dvd:
   "a mod b = 0 \<longleftrightarrow> b dvd a"
   by (auto intro: mod_0_imp_dvd)