src/HOL/Divides.thy
changeset 51173 3cbb4e95a565
parent 50422 ee729dbd1b7f
child 51299 30b014246e21
     1.1 --- a/src/HOL/Divides.thy	Sun Feb 17 20:45:49 2013 +0100
     1.2 +++ b/src/HOL/Divides.thy	Sun Feb 17 21:29:30 2013 +0100
     1.3 @@ -740,6 +740,10 @@
     1.4    shows "m mod n < (n::nat)"
     1.5    using assms divmod_nat_rel [of m n] unfolding divmod_nat_rel_def by auto
     1.6  
     1.7 +lemma mod_Suc_le_divisor [simp]:
     1.8 +  "m mod Suc n \<le> n"
     1.9 +  using mod_less_divisor [of "Suc n" m] by arith
    1.10 +
    1.11  lemma mod_less_eq_dividend [simp]:
    1.12    fixes m n :: nat
    1.13    shows "m mod n \<le> m"