added lemma
authornoschinl
Wed Jun 19 17:34:56 2013 +0200 (2013-06-19)
changeset 52398656e5e171f19
parent 52397 e95f6b4b1bcf
child 52399 7a7d05e2e5c0
added lemma
src/HOL/Divides.thy
     1.1 --- a/src/HOL/Divides.thy	Wed Jun 19 17:33:51 2013 +0200
     1.2 +++ b/src/HOL/Divides.thy	Wed Jun 19 17:34:56 2013 +0200
     1.3 @@ -1007,6 +1007,13 @@
     1.4    using mod_div_equality [of m n] by arith
     1.5  (* FIXME: very similar to mult_div_cancel *)
     1.6  
     1.7 +lemma div_eq_dividend_iff: "a \<noteq> 0 \<Longrightarrow> (a :: nat) div b = a \<longleftrightarrow> b = 1"
     1.8 +  apply rule
     1.9 +  apply (cases "b = 0")
    1.10 +  apply simp_all
    1.11 +  apply (metis (full_types) One_nat_def Suc_lessI div_less_dividend less_not_refl3)
    1.12 +  done
    1.13 +
    1.14  
    1.15  subsubsection {* An ``induction'' law for modulus arithmetic. *}
    1.16