added lemma
authornipkow
Fri Mar 06 22:06:33 2009 +0100 (2009-03-06)
changeset 303236a02238da8e9
parent 30322 90e309d20d58
child 30324 9afd9a9d0812
child 30370 79a7491ac1fd
added lemma
src/HOL/IntDiv.thy
     1.1 --- a/src/HOL/IntDiv.thy	Fri Mar 06 21:57:56 2009 +0100
     1.2 +++ b/src/HOL/IntDiv.thy	Fri Mar 06 22:06:33 2009 +0100
     1.3 @@ -1025,9 +1025,12 @@
     1.4  apply (auto simp add: div_eq_minus1)
     1.5  done
     1.6  
     1.7 -lemma div_nonneg_neg_le0: "[| (0::int) \<le> a;  b < 0 |] ==> a div b \<le> 0"
     1.8 +lemma div_nonneg_neg_le0: "[| (0::int) \<le> a; b < 0 |] ==> a div b \<le> 0"
     1.9  by (drule zdiv_mono1_neg, auto)
    1.10  
    1.11 +lemma div_nonpos_pos_le0: "[| (a::int) \<le> 0; b > 0 |] ==> a div b \<le> 0"
    1.12 +by (drule zdiv_mono1, auto)
    1.13 +
    1.14  lemma pos_imp_zdiv_nonneg_iff: "(0::int) < b ==> (0 \<le> a div b) = (0 \<le> a)"
    1.15  apply auto
    1.16  apply (drule_tac [2] zdiv_mono1)