for a, n being Nat
for p being prime Nat holds
( not p = (2 * n) + 1 or p divides a or p divides (a |^ n) - 1 or p divides (a |^ n) + 1 )