Proving the set of non-increasing finite sequences of natural numbers is well-ordered Consider the set of non-increasing sequences of natural numbers, which are constantly zero starting from some finite index (possibly different for each sequence). The ordering on this set is defined as $x_1 x_2 \ldots < y_1 y_2 \ldots \iff \exists n : x_n < y_n \land \forall i < n : x_i = y_i$. Prove this set is well-founded.
I have a few ideas about considering an arbitrary sequence of items from this set and proving that every such sequence is finite by bounding the behavior of the last non-zero element of each item and proving that it converges to 0 in a finite amount of steps, but it seems to be unnecessarily clumsy and error-prone. So, what would be a good way to prove the well-foundness?

Let $\def\C{\mathcal C}\C$ be the set of sequences satisfying your rules. Let $\C_n$ be the set of such sequences whose first term is at most $n$. Since $\C=\bigcup_{n\ge0} \C_n$, it suffices to show $\C_n$ is well ordered for each $n\ge0$. You can prove this by induction on $n$. Obviously $\C_0$ is well-founded.
Suppose by way of contradiction that $\C_n$ is not well-founded, so there is a sequence $c_1,c_2,c_3,\dots,$ of elements of $\C_n$ where $$c_1>c_2>c_3>\dots$$ Let $k$ be the number of times that $n$ occurs in $c_1$. If $k=0$, then each $c_i$ is in $\C_{n-1}$, which by induction contradicts the fact that $\C_{n-1}$ is well-founded. Otherwise, I claim that there exists some $c_i$ such that the number of times which $n$ occurs in $c_i$ is less than $k$. If not, then each $c_i$ in this sequence looks like $\overbrace{n,\dots,n}^k$, followed by some sequence $\tilde c_i\in \C_{n-1}$. But then $\tilde c_i$ would be a decreasing sequence in $\C_{n-1}$, contradiction.
Therefore, there is some $c_i$ which begins with fewer than $k$ instances of $n$. But applying the same logic, there is some $c_j$ after that which begins with even fewer $n$'s. Continuing, there must be some $c_\ell$ whose first entry is less than $n$, meaning everything afterwards is in $\C_{n-1}$, obtaining a contradiction.
