src/HOL/Divides.thy
changeset 14437 92f6aa05b7bb
parent 14430 5cb24165a2e1
child 14640 b31870c50c68
     1.1 --- a/src/HOL/Divides.thy	Fri Mar 05 15:19:55 2004 +0100
     1.2 +++ b/src/HOL/Divides.thy	Fri Mar 05 15:26:04 2004 +0100
     1.3 @@ -480,6 +480,12 @@
     1.4  apply (auto simp add: Suc_diff_le diff_less le_mod_geq)
     1.5  done
     1.6  
     1.7 +lemma nat_mod_div_trivial [simp]: "m mod n div n = (0 :: nat)"
     1.8 +by (case_tac "n=0", auto)
     1.9 +
    1.10 +lemma nat_mod_mod_trivial [simp]: "m mod n mod n = (m mod n :: nat)"
    1.11 +by (case_tac "n=0", auto)
    1.12 +
    1.13  
    1.14  subsection{*The Divides Relation*}
    1.15