Every matrix in $\mathrm{Sp}^*(2n)$ is joined to $W^+$ or $W^-$ inside $\mathrm{Sp}^*(2n)$

Let $\mathrm{Sp}^*(2n)$ be the set of real symplectic $2n\times 2n$ matrices $A$ (with respect to $J_0=\begin{pmatrix}0&-\mathrm{Id}\\ \mathrm{Id}&0\end{pmatrix}$) such that $1$ is not an eigenvalue of $A$, i.e. $\det(\mathrm{Id}-A)\neq 0$. Let $W^+=-\mathrm{Id}$ and $W^-=\mathrm{diag}(2,-1,\dots,-1,\tfrac12,-1,\dots,-1)$.

For every $A\in\mathrm{Sp}^*(2n)$ there is a continuous path $\chi:[0,1]\to\mathrm{Sp}^*(2n)$ with $\chi(0)=A$ and $\chi(1)\in\{W^+,W^-\}$.

This is the existence half of the definition of the Conley–Zehnder index: every $\psi\in\mathrm{SP}(n)$ admits an extension $\tilde\psi$ through $\mathrm{Sp}^*(2n)$ ending at $W^\pm$.

Formalization note: paths are C(unitInterval, Mat n), where Mat n is the type of real matrices indexed by Fin n ⊕ Fin n; SpStar n, Wplus n, Wminus n are from the definition module ConleyZehnder_Setting. For $n=0$ the statement is trivial.