src/HOL/Number_Theory/Cong.thy

   for a m :: int
   by (auto simp: cong_int_def)  (metis mod_mod_trivial pos_mod_conj)
 
 lemma cong_iff_lin_int: "[a = b] (mod m) \<longleftrightarrow> (\<exists>k. b = a + m * k)"
   for a b :: int
-  apply (auto simp add: cong_altdef_int dvd_def)
-  apply (rule_tac [!] x = "-k" in exI, auto)
-  done
+  by (auto simp add: cong_altdef_int algebra_simps elim!: dvdE)
+    (simp add: distrib_right [symmetric] add_eq_0_iff)
 
 lemma cong_iff_lin_nat: "([a = b] (mod m)) \<longleftrightarrow> (\<exists>k1 k2. b + k1 * m = a + k2 * m)"
   (is "?lhs = ?rhs")
   for a b :: nat
 proof

   by (metis add.right_neutral cong_0_1_nat cong_iff_lin_nat cong_to_1_nat
       dvd_div_mult_self leI le_add_diff_inverse less_one mult_eq_if)
 
 lemma cong_le_nat: "y \<le> x \<Longrightarrow> [x = y] (mod n) \<longleftrightarrow> (\<exists>q. x = q * n + y)"
   for x y :: nat
-  by (metis cong_altdef_nat Nat.le_imp_diff_is_add dvd_def mult.commute)
+  by (auto simp add: cong_altdef_nat le_imp_diff_is_add elim!: dvdE)
 
 lemma cong_solve_nat:
   fixes a :: nat
   assumes "a \<noteq> 0"
   shows "\<exists>x. [a * x = gcd a n] (mod n)"