theorem Th7: :: PEPIN:7

for m, n being Nat st m <> 0 & m divides n mod m holds
m divides n