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