theorem Th63: :: NEWTON02:161

for a being Nat
for n being prime Nat holds
( n divides (a |^ n) + 1 iff n divides a + 1 )