Assume $a\in\mathbb R,\,e^{-e}<a<e^{1/e}$ and $n\in\mathbb N$.
Let ${^n a}$ denote tetration: $${^0a}=1,\quad{^{(n+1)}a}=a^{\left({^n a}\right)}.\tag1$$ It is well known that under these assumptions, the following limit exists: $${^\infty a} = \lim_{n\to\infty}{^n a} = \frac{W\!\left(-\ln a\right)}{-\ln a} = e^{-W\left(-\ln a\right)},\tag2$$ where $W(z)$ is the Lambert $W$-function.
It is also known that $$\lim_{n\to\infty}\frac{{^\infty a} - {^{(n+1)} a}}{{^\infty a} - {^n a}} = {^\infty a} \cdot \ln a.\tag3$$
How can we prove that the following also holds?
$$\lim_{n\to\infty}\left(\frac 1 {{^\infty a} - {^n a}}-\frac{{^\infty a} - {^{(n+1)} a}}{{^\infty a} \cdot \left({^\infty a} - {^n a}\right)^2 \cdot \ln a}\right)=\frac{\ln a}2\tag4$$