# HG changeset patch
# User noschinl
# Date 1371656096 -7200
# Node ID 656e5e171f19338cfe4000e844cb197aca3c762b
# Parent  e95f6b4b1bcfd67101090b40d451497a20c73494
added lemma

diff -r e95f6b4b1bcf -r 656e5e171f19 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Wed Jun 19 17:33:51 2013 +0200
+++ b/src/HOL/Divides.thy	Wed Jun 19 17:34:56 2013 +0200
@@ -1007,6 +1007,13 @@
   using mod_div_equality [of m n] by arith
 (* FIXME: very similar to mult_div_cancel *)
 
+lemma div_eq_dividend_iff: "a \<noteq> 0 \<Longrightarrow> (a :: nat) div b = a \<longleftrightarrow> b = 1"
+  apply rule
+  apply (cases "b = 0")
+  apply simp_all
+  apply (metis (full_types) One_nat_def Suc_lessI div_less_dividend less_not_refl3)
+  done
+
 
 subsubsection {* An ``induction'' law for modulus arithmetic. *}