Let $\mathcal{R}$ an o-minimal expansion of $\overline{\mathbb{R}}$ and $g$ a unary definable function such that $g'\sim 1/x$ (by the monotonicity theorem $g$ is ultimately differentiable)
By applying the mean value theorem on $g$ (by the monotonicity theorem $g$ is ultimately differentiable) there exists a function $f$ ultimatly defined such that $$g(2x)-g(x)=x\cdot g'(f(x))$$
My question : Why is f definable?
My argument : By applying the monotonicity theorem on $g'$ (the derivative of a definable function is definable) $g'$ is either constant or strictly monotone. By the assumption $g'\sim 1/x$ , $g'$ cant be a constant. hence $(g')^{-1}$ is ultimately defined. thus we have ultimatly $$(g')^{-1}(\frac{g(2x)-g(x)}{x})=f(x)$$
Hence $f$ is definable as compsition of definable functions.
Is my argument good?