theorem Th15: :: NAT_4:15

for a, p, k being Nat st (a |^ k) mod p = 1 & k >= 1 & p is prime holds
a,p are_coprime