In page 213(63) of the paper Spectral properties of Schrödinger operators and scattering theory by Shmuel Agmon, he used a stronger result of the implicit function theorem, which I'll state below in dimension 2:
Theorem: Let $F=F(x,y)\in C^\infty(\mathbb R^2)$ and $F(x_0,y_0)=0$. If $\frac{\partial F}{\partial x}(x_0,y_0)\neq 0$, then there exists $\delta>0$ such that in the small ball $B_\delta=\{(x,y):|(x,y)-(x_0,y_0)|<\delta\}$ the function $F$ admits a factorization $$F(x,y)=G(x,y)(x-g(y)),$$ where $G\in C^\infty(B_\delta)$, $G\neq 0$ in $B_\delta$, and $g(y)$ is a smooth function of $y$ for $|y-y_0|<\delta$.
By the classical implicit function theorem, there exists a smooth function $g=g(y)$ near $y_0$ such that the solution of the equation $F(x,y)=0$ is given by $x=g(y)$ near $(x_0,y_0)$. But this is not stronger enough to derive the above result.
So I'm asking about the proof of the above theorem, which is a stronger result about Implicit Function Theorem. Any hint of the proof or available reference would be very appreciated.
Attempt at proof: A smooth change of coordinates turns the zero set locally into a straight vertical line passing through $x=0$ ie $g(y)=0$. Now set $$G(x,y)=\begin{cases}F(x,y)/x&x\neq0\\F_x(0,y)&x=0\end{cases}.$$ $G$ doesn’t vanish by construction. It is at least continuous, by l’Hopital. Then you can check $G_y$ is continuous, and $G_x(0,y)$ exists, again by l’Hopital. Arrange it in an induction and undo the change of coordinates and I think that’s it.