for a, n being Nat st a > 1 holds
a - 1 divides (a |^ n) - 1