src/HOL/Number_Theory/Residues.thy
changeset 66954 0230af0f3c59
parent 66888 930abfdf8727
child 67051 e7e54a0b9197
     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Mon Oct 30 19:29:06 2017 +0000
     1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Tue Oct 31 07:11:03 2017 +0000
     1.3 @@ -291,8 +291,8 @@
     1.4  next
     1.5    case False
     1.6    with assms show ?thesis
     1.7 -    using residues.euler_theorem [of "int m" "int a"] transfer_int_nat_cong
     1.8 -    by (auto simp add: residues_def gcd_int_def) force
     1.9 +    using residues.euler_theorem [of "int m" "int a"] cong_int_iff
    1.10 +    by (auto simp add: residues_def gcd_int_def) fastforce
    1.11  qed
    1.12  
    1.13  lemma fermat_theorem: