src/HOL/Number_Theory/Residues.thy

   case True
   then show ?thesis by auto
 next
   case False
   with assms show ?thesis
-    using residues.euler_theorem [of "int m" "int a"] transfer_int_nat_cong
-    by (auto simp add: residues_def gcd_int_def) force
+    using residues.euler_theorem [of "int m" "int a"] cong_int_iff
+    by (auto simp add: residues_def gcd_int_def) fastforce
 qed
 
 lemma fermat_theorem:
   fixes p a :: nat
   assumes "prime p" and "\<not> p dvd a"