I am looking for further proofs, preferably in the literature, of the following result:
Proposition: Let $R$ be a unital commutative $\mathbb{Z}$-torsion free ring. If $f(x) \in R[x]$ with $f'(x) \in U(R[x])$, then there exists $g(x) \in R[x]$ such that $f(g(x)) = g(f(x)) = x$ in $R[x]$.
For example, $R = \mathbb{Z}$ is allowed (mixed characteristic) as well as $R = \mathbb{Z}[t]/(t^2)$, but $R = \mathbb{Z} \times \mathbb{Z} /(n)$ is not allowed.
I already have a proof of this fact which relies explicitly on a theorem of Comtet mentioned at least in MO415617, MO337330, and MO80828. So, if there is a proof in the literature based on a Comtet's type of result, I would like to know about this reference, but I am mostly interested in "new" proofs that do not invoke this type of result.
The $1$-dimensional Jacobian Problem in for $\mathbb{Z}$-torsion free rings as stated above should be well-known to experts (as a non-problem). But one issue when searching through the literature is that people are understandably mostly focused on the complex case in higher dimensions. Indeed the above result is completely trivial for any ring with $\operatorname{nil}(R) = 0$, not just $\mathbb{C}$.
EDIT: By Remy van Dobben de Bruyn's comment below, the name $\mathbb{Z}$-torsion free is a much more standard name than what I called strong characteristic 0 previously. Requiring only characteristic 0 is insufficient as shown by his example in the comments, but on the other hand requiring $R$ to be a $\mathbb{Q}$-algebra is a tad too strong as it excludes too many valid examples like the ones mentioned above. The point is that it suffices that multiplication by non-zero integers has a trivial kernel rather than non-zero integers being invertible in $R$.