for k, n being Nat st n <> 0 & 1 <= k holds
(n |^ k) div n = n |^ (k -' 1)