changeset 30840 | 98809b3f5e3c |
parent 30837 | 3d4832d9f7e4 |
child 30923 | 2697a1d1d34a |
--- a/src/HOL/Divides.thy Wed Apr 01 16:55:31 2009 +0200 +++ b/src/HOL/Divides.thy Wed Apr 01 18:41:15 2009 +0200 @@ -827,6 +827,9 @@ lemma nat_div_eq_0 [simp]: "(n::nat) > 0 ==> ((m div n) = 0) = (m < n)" by(auto, subst mod_div_equality [of m n, symmetric], auto) +lemma nat_div_gt_0 [simp]: "(n::nat) > 0 ==> ((m div n) > 0) = (m >= n)" +by (subst neq0_conv [symmetric], auto) + declare div_less_dividend [simp] text{*A fact for the mutilated chess board*}