for a, n being Nat st (2 * n) + 1 is prime holds
for k being Nat st 2 * n > k & k > 1 holds
( not (2 * n) + 1 divides (a |^ n) - k & not (2 * n) + 1 divides (a |^ n) + k )