theorem :: PEPIN:14

for i, j, k being Nat st k ^2 < j & i mod j = k holds
(i ^2) mod j = k ^2