diff -r 46c8969a995b -r 653de351d21c src/HOL/Number_Theory/Residues.thy
--- a/src/HOL/Number_Theory/Residues.thy	Fri Jan 31 19:32:13 2014 +0100
+++ b/src/HOL/Number_Theory/Residues.thy	Sat Feb 01 00:32:32 2014 +0000
@@ -372,6 +372,12 @@
   finally show ?thesis .
 qed
 
+lemma fermat_theorem_nat:
+  assumes "prime p" and "~ (p dvd a)"
+  shows "[a^(p - 1) = 1] (mod p)"
+using fermat_theorem [of p a] assms
+by (metis int_1 nat_int of_nat_power prime_int_def transfer_int_nat_cong zdvd_int)
+
 
 subsection {* Wilson's theorem *}