theorem :: NEWTON02:78

for a, k being Nat
for n being positive Nat holds
( a divides k * ((a |^ n) + 1) iff a divides k )