theorem lemdiv: :: NUMBER01:11

for a being Integer
for m being Nat holds a - 1 divides (a |^ m) - 1