--- 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)