for a, n being Nat st a <> 0 holds
n divides n |^ a