some new results

--- a/src/HOL/Divides.thy	Fri Mar 05 15:19:55 2004 +0100
+++ b/src/HOL/Divides.thy	Fri Mar 05 15:26:04 2004 +0100
@@ -480,6 +480,12 @@
 apply (auto simp add: Suc_diff_le diff_less le_mod_geq)
 done
 
+lemma nat_mod_div_trivial [simp]: "m mod n div n = (0 :: nat)"
+by (case_tac "n=0", auto)
+
+lemma nat_mod_mod_trivial [simp]: "m mod n mod n = (m mod n :: nat)"
+by (case_tac "n=0", auto)
+
 
 subsection{*The Divides Relation*}