IMO 1993 b2 proof

Question

"Let $\mathbb{N}=\{ 1,2,3,\ldots \}$. Determine if there exists a strictly increasing function $f:\mathbb{N}\to\mathbb{N}$ such that

1) $f(1)=2$

2) $f(f(n))=f(n)+n$ for all $n$."

Of the solutions I've seen online, one such $f(n)$ that should work is $$f(n)=\left[\phi n + \frac{1}{2}\right]$$ where $\phi\approx 1.618$ is the golden ratio and the square brackets denote the integral part. It is easy to see that $f(1)=2$ and that $f(n)$ is strictly increasing - however the proof that this satisfies condition 2 seems to be incorrect or unclear in the sources I have found. A clear proof that this $f(n)$ satisfies 2) would be appreciated.

Answer 1

Never mind, it makes sense now (not my solution, just a rewrite).

Claim: $f(n)=\left[\phi n + \frac{1}{2}\right]$ satisfies $f(f(n))=f(n)+n$.

Now $f(f(n))-f(n)-n=\left[\phi\left[\phi n+\frac{1}{2}\right] +\frac{1}{2}\right]-\left[\phi n +\frac{1}{2}\right]-n$, so it suffices to show $X(n)=\phi\left[\phi n + \frac{1}{2}\right]+\frac{1}{2}-\left[\phi n +\frac{1}{2}\right]-n=(\phi-1)\left[\phi n +\frac{1}{2}\right]+\frac{1}{2}-n$ satisfies $0\leq X(n) < 1$.

For the lower bound, $\left[\phi n +\frac{1}{2}\right]\geq \phi n -\frac{1}{2}$, giving $$X(n)\geq \phi^2n-\frac{\phi}{2}-\phi n+1-n.$$ But $\phi=\frac{1+\sqrt{5}}{2}$, so $n(\phi^2-\phi-1)=0$. Hence $X(n)\geq 1-\frac{\phi}{2}>0.$ For the upper bound, $\left[\phi n +\frac{1}{2}\right] \leq \phi n + \frac{1}{2}$, giving $$X(n)\leq \phi^2 n+\frac{\phi}{2}-\phi n-n=\frac{\phi}{2}<1$$ as required.