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*}