added lemma
authorhaftmann
Sun Aug 18 15:29:50 2013 +0200 (2013-08-18)
changeset 530661f61a923c2d6
parent 53065 de1816a7293e
child 53067 ee0b7c2315d2
added lemma
src/HOL/Divides.thy
     1.1 --- a/src/HOL/Divides.thy	Sun Aug 18 15:29:50 2013 +0200
     1.2 +++ b/src/HOL/Divides.thy	Sun Aug 18 15:29:50 2013 +0200
     1.3 @@ -733,6 +733,17 @@
     1.4  lemma div_mult_self1_is_m [simp]: "0<n ==> (n*m) div n = (m::nat)"
     1.5  by simp
     1.6  
     1.7 +lemma div_positive:
     1.8 +  fixes m n :: nat
     1.9 +  assumes "n > 0"
    1.10 +  assumes "m \<ge> n"
    1.11 +  shows "m div n > 0"
    1.12 +proof -
    1.13 +  from `m \<ge> n` obtain q where "m = n + q"
    1.14 +    by (auto simp add: le_iff_add)
    1.15 +  with `n > 0` show ?thesis by simp
    1.16 +qed
    1.17 +
    1.18  
    1.19  subsubsection {* Remainder *}
    1.20