A stronger result about Implicit Function Theorem: Factorization $F(x,y)=G(x,y)(x-g(y))$ 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.
 A: 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.
A: My classmate shows me a direct proof using Taylor's formula. Recall Taylor's formula:

If $f\in C^\infty(\mathbb R)$, then for all $x,x_0\in \mathbb R$ we have
\begin{align*}
f(x)&=f(x_0)+f'(x_0)(x-x_0)+\int_{x_0}^x f''(t)(x-t)\,dt\\
&=f(x_0)+f'(x_0)(x-x_0)+(x-x_0)^2\int_0^1f''\left(x_0+s(x-x_0)\right)(1-s)\,ds.
\end{align*}

Now near the zero point $(x_0,y_0)$ of $F$ we have
$$F(x,y)=F(g(y),y)+\frac{\partial F}{\partial x}(g(y),y)(x-g(y))+\left(x-g(y)\right)^2\int_0^1\frac{\partial^2F}{\partial x^2}\left(g(y)+s(x-g(y)),y\right)(1-s)\,ds.$$
Note that $F(g(y),y)=0$, so $F(x,y)=G(x,y)(x-g(y))$, where
$$G(x,y)=\frac{\partial F}{\partial x}(g(y),y)+(x-g(y))\int_0^1\frac{\partial^2F}{\partial x^2}\left(g(y)+s(x-g(y)),y\right)(1-s)\,ds.$$
Clearly, $G$ is smooth near $(x_0,y_0)$. Since $G(x_0,y_0)=\frac{\partial F}{\partial x}(x_0,y_0)\neq0$, $G\neq0$ near $(x_0,y_0)$. This completes the proof.
