| changeset 14437 | 92f6aa05b7bb |
| parent 14430 | 5cb24165a2e1 |
| child 14640 | b31870c50c68 |
--- 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*}