# HG changeset patch
# User haftmann
# Date 1376832590 -7200
# Node ID 1f61a923c2d60be2c9ef287e70f6874987897efb
# Parent  de1816a7293eb1610777de6410d91f5723eeb5c6
added lemma

diff -r de1816a7293e -r 1f61a923c2d6 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sun Aug 18 15:29:50 2013 +0200
+++ b/src/HOL/Divides.thy	Sun Aug 18 15:29:50 2013 +0200
@@ -733,6 +733,17 @@
 lemma div_mult_self1_is_m [simp]: "0<n ==> (n*m) div n = (m::nat)"
 by simp
 
+lemma div_positive:
+  fixes m n :: nat
+  assumes "n > 0"
+  assumes "m \<ge> n"
+  shows "m div n > 0"
+proof -
+  from `m \<ge> n` obtain q where "m = n + q"
+    by (auto simp add: le_iff_add)
+  with `n > 0` show ?thesis by simp
+qed
+
 
 subsubsection {* Remainder *}