theorem Th39: :: PEPIN:39

for m, n being Nat st n > 1 holds
( m mod n = 1 iff m,1 are_congruent_mod n )