theorem :: PEPIN:15

for i, p being Nat st p is prime & i mod p = - 1 holds
(i ^2) mod p = 1