# HG changeset patch
# User huffman
# Date 1235426136 28800
# Node ID beee83623cc91689705f62c89824265d480be01c
# Parent  c5920259850c3e7559c7600b34bc76bb30d52ce0
move lemma dvd_mod_imp_dvd into class semiring_div

diff -r c5920259850c -r beee83623cc9 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Mon Feb 23 21:38:45 2009 +0100
+++ b/src/HOL/Divides.thy	Mon Feb 23 13:55:36 2009 -0800
@@ -194,6 +194,12 @@
 apply(fastsimp simp add: mult_assoc)
 done
 
+lemma dvd_mod_imp_dvd: "[| k dvd m mod n;  k dvd n |] ==> k dvd m"
+  apply (subgoal_tac "k dvd (m div n) *n + m mod n")
+   apply (simp add: mod_div_equality)
+  apply (simp only: dvd_add dvd_mult)
+  done
+
 text {* Addition respects modular equivalence. *}
 
 lemma mod_add_left_eq: "(a + b) mod c = (a mod c + b) mod c"
@@ -848,12 +854,6 @@
   apply (blast intro: mod_mult_distrib2 [symmetric])
   done
 
-lemma dvd_mod_imp_dvd: "[| (k::nat) dvd m mod n;  k dvd n |] ==> k dvd m"
-  apply (subgoal_tac "k dvd (m div n) *n + m mod n")
-   apply (simp add: mod_div_equality)
-  apply (simp only: dvd_add dvd_mult)
-  done
-
 lemma dvd_mod_iff: "k dvd n ==> ((k::nat) dvd m mod n) = (k dvd m)"
 by (blast intro: dvd_mod_imp_dvd dvd_mod)