Problem: Let $n$ be a positive integer.
Define a sequence by setting $a_1 = n$ and, for each $k > 1$,
letting $a_k$ be the unique integer in the range $0 \leq a_k \leq k-1$
for which $a_1 + a_2 + \dots + a_k$ is divisible by $k$.
(For instance, when $n = 9$
the obtained sequence is $9,1,2,0,3,3,3,\dots$.)
Prove that for any $n$ the sequence $a_1$, $a_2$, \dots
eventually becomes constant.

Solution: For each $k$, the number
\[ b_k \coloneq \frac 1k (a_1 + \dots + a_k) \]
is a nonnegative integer.
\begin{claim*}
  The sequence $(b_k)$ is eventually constant.
\end{claim*}
\begin{proof}
  Since
  \[ b_{k+1}
    = \frac{a_1 + \dots + a_k + a_{k+1}}{k+1}
    \le \frac{k b_k + k}{k+1} < b_k + 1 \]
  and therefore $b_{k+1} \le b_k$ for all $k$.
  Hence the sequence $b_k$ must eventually be constant.
\end{proof}

This can only happen once the sequence is constant:
indeed if $N$ is an index such that $b_N = b_{N+1} = \dots = b$ then
\[ a_k = (k+1) b_{k+1} - k \cdot b_k
  = (k+1) \cdot b - k \cdot b = b \]
for any $k \ge N$.
In other words, $a_N = a_{N+1} = \dots = b$ as well.