# HG changeset patch
# User nipkow
# Date 1238604075 -7200
# Node ID 98809b3f5e3cc01b132f6baef149a0732990a827
# Parent  bf99ceb7d01537a8a8f860eab600f8a73d335a03
added  nat_div_gt_0 [simp]

diff -r bf99ceb7d015 -r 98809b3f5e3c src/HOL/Divides.thy
--- 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*}