--- a/src/HOL/Number_Theory/Cong.thy Thu Oct 31 16:54:22 2013 +0100
+++ b/src/HOL/Number_Theory/Cong.thy Fri Nov 01 18:51:14 2013 +0100
@@ -543,7 +543,8 @@
apply (subgoal_tac "a * b = (-a * -b)")
apply (erule ssubst)
apply (subst zmod_zmult2_eq)
- apply (auto simp add: mod_add_left_eq)
+ apply (auto simp add: mod_add_left_eq mod_minus_right div_minus_right)
+ apply (metis mod_diff_left_eq mod_diff_right_eq mod_mult_self1_is_0 semiring_numeral_div_class.diff_zero)+
done
lemma cong_to_1_nat: "([(a::nat) = 1] (mod n)) \<Longrightarrow> (n dvd (a - 1))"