# HG changeset patch # User haftmann # Date 1376832590 -7200 # Node ID 1f61a923c2d60be2c9ef287e70f6874987897efb # Parent de1816a7293eb1610777de6410d91f5723eeb5c6 added lemma diff -r de1816a7293e -r 1f61a923c2d6 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Sun Aug 18 15:29:50 2013 +0200 +++ b/src/HOL/Divides.thy Sun Aug 18 15:29:50 2013 +0200 @@ -733,6 +733,17 @@ lemma div_mult_self1_is_m [simp]: "0 (n*m) div n = (m::nat)" by simp +lemma div_positive: + fixes m n :: nat + assumes "n > 0" + assumes "m \ n" + shows "m div n > 0" +proof - + from `m \ n` obtain q where "m = n + q" + by (auto simp add: le_iff_add) + with `n > 0` show ?thesis by simp +qed + subsubsection {* Remainder *}