[isabelle] "[|prime p |] ==>(n::nat)^p = n mod p"



What is an elegant and compact way to prove (Fermat's little theorem for natural numbers)

lemma "[|prime p |] ==>(n::nat)^p = n mod p"

in Isabelle.  Would appreciate a code snippet

Regards
Srinivas





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.