for n, p being Nat st p is prime & n,p are_coprime holds
(n |^ (p -' 1)) mod p = 1