Nonsingular point with $\partial_0 h(z) \neq 0$ forces infinite zero set

Let $h$ be a plane polynomial ($h : \mathrm{PlanePoly}$), $z$ a point of the plane with $h_z : z \in \mathrm{PlaneCurveZeroSet}\,h$, and suppose the partial derivative in the first variable does not vanish at $z$:

Then the zero set of $h$ is infinite:

This is one of the two nonsingularity-implies-infinite-curve lemmas (here for $\partial_0$). The underlying tool is the smooth ($C^\infty$, ContDiff) implicit function theorem, invoked through ContDiffAt.implicitFunction: a point where a partial derivative is nonzero lies on a locally graphed segment of the curve, so the curve is infinite. The $\partial_0$ case is obtained from the $\partial_1$ case by renaming the two variables of $h$ with the swap and moving points with $\mathrm{swapPoint}$. It supports the fact that a finite real zero set consists entirely of singular points, which is needed to count singularities of irreducible curves.