# HG changeset patch
# User nipkow
# Date 1236373593 -3600
# Node ID 6a02238da8e9a63c61691a9993e98c2c0d14474d
# Parent  90e309d20d58228af2074168424cfe7f6e21474d
added lemma

diff -r 90e309d20d58 -r 6a02238da8e9 src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Fri Mar 06 21:57:56 2009 +0100
+++ b/src/HOL/IntDiv.thy	Fri Mar 06 22:06:33 2009 +0100
@@ -1025,9 +1025,12 @@
 apply (auto simp add: div_eq_minus1)
 done
 
-lemma div_nonneg_neg_le0: "[| (0::int) \<le> a;  b < 0 |] ==> a div b \<le> 0"
+lemma div_nonneg_neg_le0: "[| (0::int) \<le> a; b < 0 |] ==> a div b \<le> 0"
 by (drule zdiv_mono1_neg, auto)
 
+lemma div_nonpos_pos_le0: "[| (a::int) \<le> 0; b > 0 |] ==> a div b \<le> 0"
+by (drule zdiv_mono1, auto)
+
 lemma pos_imp_zdiv_nonneg_iff: "(0::int) < b ==> (0 \<le> a div b) = (0 \<le> a)"
 apply auto
 apply (drule_tac [2] zdiv_mono1)