src/HOL/Divides.thy
changeset 52398 656e5e171f19
parent 51717 9e7d1c139569
child 52435 6646bb548c6b
--- 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. *}