src/HOL/Divides.thy
changeset 53066 1f61a923c2d6
parent 52435 6646bb548c6b
child 53067 ee0b7c2315d2
     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