theorem Th3: :: PEPIN:3

for k, m, n being Nat st k divides n * m & n,k are_coprime holds
k divides m