# HG changeset patch
# User paulson
# Date 1078496764 -3600
# Node ID 92f6aa05b7bbbe6bcf96c0c1387e030adf776023
# Parent  77017c49c0041b3c459f710b8bed2d68f545fb7f
some new results

diff -r 77017c49c004 -r 92f6aa05b7bb src/HOL/Divides.thy
--- 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*}