theorem :: PEPIN:8

for m, n, k being Nat st 0 < n & m mod n = k holds
n divides m - k