src/HOL/NumberTheory/EulerFermat.thy

    apply (simp only: zcong_def)
    apply (subgoal_tac "zgcd a m = m")
     prefer 2
     apply (subst zdvd_iff_zgcd [symmetric])
      apply (rule_tac [4] zgcd_zcong_zgcd)
-       apply (simp_all add: zdvd_zminus_iff zcong_sym)
+       apply (simp_all add: zcong_sym)
   done
 
 
 text {* \medskip @{term noXRRset} *}