for m being positive Integer
for a being Nat st a > 1 holds
(((a |^ m) - 1) div (a - 1)) gcd (a - 1) = (a - 1) gcd m