theorem :: PEPIN:13

for i being Nat st i <> 0 holds
(i ^2) mod (i + 1) = 1