Uniqueness of the local index of an isolated zero

Let $f:\mathbb{C}\to\mathbb{C}$ and $z_0\in\mathbb{C}$. If $z_0$ is an isolated zero of $f$ of local index $k$ and also of local index $m$, then $k=m$.

This makes the local index of an isolated zero a well-defined integer, so that index sums such as $\mathrm{wind}_\pi$ (Hryniewicz (14)) do not depend on the chosen witnesses.

Formalization Note "Isolated zero of local index $k$" is HasZeroIndex f z₀ k: $f(z_0)=0$, $f$ has no other zero in some closedBall z₀ r with $r>0$, and every counterclockwise circle $t\mapsto z_0+\rho e^{2\pi i t}$ with $0<\rho<r$ has winding number $k$ under $f$ (HasLoopWind).