theorem Th11: :: PEPIN:11

for k, m, n being Nat st 1 < m & (n * k) mod m = k mod m & k,m are_coprime holds
n mod m = 1