src/HOL/Divides.thy

--- a/src/HOL/Divides.thy	Fri Feb 20 16:48:17 2009 +0100
+++ b/src/HOL/Divides.thy	Fri Feb 20 20:50:49 2009 +0100
@@ -795,12 +795,6 @@
 apply (auto simp add: Suc_diff_le le_mod_geq)
 done
 
-lemma nat_mod_div_trivial: "m mod n div n = (0 :: nat)"
-by simp
-
-lemma nat_mod_mod_trivial: "m mod n mod n = (m mod n :: nat)"
-by simp
-
 
 subsubsection {* The Divides Relation *}