theorem Th27: :: GR_CY_3:27
for a, n being Nat holds a - 1 divides (a |^ n) - 1