A Strange Recursive Relation, Automatic

Hofstadter mentions the following recursive relation in his great book "Gödel, Escher, Bach": $$\begin{align} g(0) &= 0;\\ g(n) &= n-g(g(n-1)). \end{align}$$ I claim that $g(n) = \left\lfloor \phi\cdot (n+1) \right\rfloor$, where $\phi = \frac{-1+\sqrt{5}}{2}$, and I'll show this using a technique that makes proving many identities of this type nearly automatic.

Let $\phi\cdot n = \left\lfloor \phi\cdot n \right\rfloor + e$, where $0 < e < 1$ as $\phi$ is irrational, nor can $e = 1-\phi$, and note that $\phi$ satisfies ${\phi}^2 + \phi - 1 = 0$. Some algebra gives $$\begin{align} n-\left\lfloor \left( \left\lfloor \phi\cdot n \right\rfloor + 1 \right) \cdot \phi \right\rfloor &= n-\left\lfloor \left( n\cdot \phi - e + 1 \right) \cdot \phi \right\rfloor \\ &= n-\left\lfloor n\cdot {\phi}^2 - e\cdot \phi + \phi \right\rfloor \\ &= n-\left\lfloor n\cdot \left(1-\phi\right) - e\cdot \phi + \phi \right\rfloor \\ &= n-n-\left\lfloor -n\cdot \phi - e\cdot \phi + \phi \right\rfloor \\ &= -\left\lfloor -n\cdot \phi - e\cdot \phi + \phi \right\rfloor \\ &= -\left\lfloor -n \cdot \phi + e - e - e\cdot \phi + \phi \right\rfloor \\ &= \left\lfloor \phi\cdot n \right\rfloor -\left\lfloor - e - e\cdot \phi + \phi \right\rfloor. \end{align}$$
Now if $$\begin{align} 0 < e < 1-\phi &\implies 0 < - e - e\cdot \phi + \phi < \phi;\\ 1-\phi < e < 1 &\implies -1 < - e - e\cdot \phi + \phi < 0. \end{align}$$
This implies $$n-\left\lfloor \left( \left\lfloor \phi\cdot n \right\rfloor + 1 \right) \cdot \phi \right\rfloor = \left\lfloor \phi\cdot (n+1) \right\rfloor .$$ Since $\left\lfloor \phi\cdot (0+1) \right\rfloor = 0$, we're done.

The point of the algebra was to move all terms involving $n$ out, and then checking to see how the remaining term varied with $e$. A simple idea, but very useful.