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