--- a/src/HOL/Divides.thy Thu Dec 17 15:22:27 2009 +0100
+++ b/src/HOL/Divides.thy Fri Dec 18 12:00:29 2009 +0100
@@ -2443,6 +2443,17 @@
declare dvd_eq_mod_eq_0_number_of [simp]
+subsubsection {* Nitpick *}
+
+lemma zmod_zdiv_equality':
+"(m\<Colon>int) mod n = m - (m div n) * n"
+by (rule_tac P="%x. m mod n = x - (m div n) * n"
+ in subst [OF mod_div_equality [of _ n]])
+ arith
+
+lemmas [nitpick_def] = mod_div_equality' [THEN eq_reflection]
+ zmod_zdiv_equality' [THEN eq_reflection]
+
subsubsection {* Code generation *}
definition pdivmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where