theorem :: PEPIN:9

for i, k, p being Nat st i * p <> 0 & k mod (i * p) < p holds
k mod (i * p) = k mod p