Solution (source code)

= Solution

If a finitely generated <Coxeter group> $W$ is finite, its integer-valued <Coxeter length> has a maximum. Conversely, if some $w_0$ has globally maximal length $N$, every group element has a word of length at most $N$. There are only finitely many words of bounded length in the finite set of simple generators, so $W$ is finite.

Realize the finite group as the <reflection group of a root system> with fundamental system $\Delta$ and positive system $\Pi$. Maximality and the fact that multiplication by a simple generator changes Coxeter length by one give
$$
\ell(w_0s_\alpha)=\ell(w_0)-1
\qquad(\alpha\in\Delta).
$$
The <positive-root criterion for Coxeter length> therefore gives $w_0\Delta\subseteq-\Pi$. Since $w_0\Delta$ is itself fundamental, it must be the simple system $-\Delta$ of the positive system $-\Pi$.

If $v_0$ is another maximal-length element, the same argument gives $v_0\Delta=-\Delta=w_0\Delta$. Hence $v_0^{-1}w_0$ stabilizes $\Delta$, and part c gives $v_0^{-1}w_0=1$. The <Longest element of a finite Coxeter group> is therefore unique.