equal
deleted
inserted
replaced
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: |