1.1 --- a/src/HOL/Divides.thy	Wed Apr 01 16:55:31 2009 +0200
     1.2 +++ b/src/HOL/Divides.thy	Wed Apr 01 18:41:15 2009 +0200
     1.3 @@ -827,6 +827,9 @@
     1.4  lemma nat_div_eq_0 [simp]: "(n::nat) > 0 ==> ((m div n) = 0) = (m < n)"
     1.5  by(auto, subst mod_div_equality [of m n, symmetric], auto)
     1.6  
     1.7 +lemma nat_div_gt_0 [simp]: "(n::nat) > 0 ==> ((m div n) > 0) = (m >= n)"
     1.8 +by (subst neq0_conv [symmetric], auto)
     1.9 +
    1.10  declare div_less_dividend [simp]
    1.11  
    1.12  text{*A fact for the mutilated chess board*}