src/HOL/Divides.thy
 changeset 52398 656e5e171f19 parent 51717 9e7d1c139569 child 52435 6646bb548c6b
equal inserted replaced
52397:e95f6b4b1bcf 52398:656e5e171f19
`  1004   using mod_div_equality [of m n] by arith`
`  1004   using mod_div_equality [of m n] by arith`
`  1005 `
`  1005 `
`  1006 lemma div_mod_equality': "(m::nat) div n * n = m - m mod n"`
`  1006 lemma div_mod_equality': "(m::nat) div n * n = m - m mod n"`
`  1007   using mod_div_equality [of m n] by arith`
`  1007   using mod_div_equality [of m n] by arith`
`  1008 (* FIXME: very similar to mult_div_cancel *)`
`  1008 (* FIXME: very similar to mult_div_cancel *)`
`       `
`  1009 `
`       `
`  1010 lemma div_eq_dividend_iff: "a \<noteq> 0 \<Longrightarrow> (a :: nat) div b = a \<longleftrightarrow> b = 1"`
`       `
`  1011   apply rule`
`       `
`  1012   apply (cases "b = 0")`
`       `
`  1013   apply simp_all`
`       `
`  1014   apply (metis (full_types) One_nat_def Suc_lessI div_less_dividend less_not_refl3)`
`       `
`  1015   done`
`  1009 `
`  1016 `
`  1010 `
`  1017 `
`  1011 subsubsection {* An ``induction'' law for modulus arithmetic. *}`
`  1018 subsubsection {* An ``induction'' law for modulus arithmetic. *}`
`  1012 `
`  1019 `
`  1013 lemma mod_induct_0:`
`  1020 lemma mod_induct_0:`