USAMO 2007 — Days 1 and 2 Question 1

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,\ldots$ eventually becomes constant.

Proposed by Sam Vandervelde; source discussion: https://aops.com/community/p825490