theorem Th27: :: GR_CY_3:27

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