--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy Sun Oct 16 09:31:05 2016 +0200
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Sun Oct 16 09:31:05 2016 +0200
@@ -510,7 +510,7 @@
also have "r' - r' div r * r = r' mod r" using div_mult_mod_eq [of r' r]
by (simp add: algebra_simps)
finally show "(s' - r' div r * s) * a + (t' - r' div r * t) * b = r' mod r" .
- qed (auto simp: gcd_eucl_non_0 algebra_simps div_mod_equality')
+ qed (auto simp: gcd_eucl_non_0 algebra_simps minus_mod_eq_div_mult [symmetric])
finally show ?thesis .
qed
qed