Conjecture about polynomials $f_n\in\mathbb Q[X_1,\dots,X_n]$ defining bijections $\mathbb N^n\to\mathbb N$ This is inspired by an answer of a question of mine:
Bijective polynomials $f\in\mathbb Q[X_1,\dots,X_n]$
There is a polynomial $f_1\in\mathbb Q[X_1]$ which define a bijection $f_1:\mathbb N\to\mathbb N$, $f_1(X_1)=X_1$.  
There is a polynomial $f_2\in\mathbb Q[X_1,X_2]$ which define a bijection $f_2:\mathbb N^2\to\mathbb N$,  
$\displaystyle f_2(X_1,X_2)=\frac{(X_1+X_2)(X_1+X_2+1)}{2}+f_1(X_1)$.  
And as far as I understand and have tested there is a polynomial $f_3\in\mathbb Q[X_1,X_2,X_3]$ which define a bijection
$f_3:\mathbb N^3\to\mathbb N$ 
$\displaystyle f_3(X_1,X_2,X_3)=\frac{(X_1+X_2+X_3)(X_1+X_2+X_3+1)(X_1+X_2+X_3+2)}{6}+f_2(X_1,X_2)$.
This seems possible to generalize as  
$\displaystyle f_{n+1}(X_1,\dots ,X_{n+1})=f_{n}(X_1,\dots ,X_{n})+\frac{1}{(n+1)!}\prod_{k=1}^{n+1}\Big(k-1+\sum_{i=1}^{n+1}X_i\Big)$.
This is a generalisation of the diagonalization in case of $n=2$ with "triangularization", "tetraederization" or higher. Now the conjecture is

$\displaystyle f_n(X_1,\dots,X_n)$ define a bijection $\mathbb N^n\to\mathbb N$ for all $n>0$.


Induction seems natural but how to prove that $f_n$ is a bijection implies that $f_{n+1}$ is a bijection?
What I want are proofs, parts of proofs or counter proofs.
 A: The diagonalization argument can indeed be generalized.  Roughly, one can see all elements of $\mathbb{N}$ appear in order by going through all hyperplanes $X_1+\ldots+X_n = s$.
Now for the proof.  Let $s=X_1+...+X_n$.  Then your function $f_n$ can be written as
$$ f_n(X_1, ..., X_n) = \binom{s+n-1}{n} + f_{n-1}(X_1, \ldots, X_{n-1}),  $$
with the conventions that $f_n(0,\ldots, 0) = 0$ and $f_0 = 0$.
Claim: Fix $s\in \mathbb{N}$.  Then $f_n$ induces a bijection 
$$ \Big\{ (X_1, \ldots, X_n)\in \mathbb{N}^n \ | \ s=X_1+...+X_n \Big\} \xrightarrow{f_n} \Big[ \binom{s+n-1}{n}, \binom{s+n}{n} -1\Big],  $$
where $[x,y]$ is the set of integers from $x$ to $y$, and if $s=0$, then the set on the right is $[0,0]$ by convention.
Proof of the claim. It is obviously true for $n=1$.  Assume it is true for $n-1$.  Let us show it is true for $n$.
For a fixed $s=X_1+...+X_n$, the value $t=X_1 + \ldots + X_{n-1}$ can be anything from $0$ to $s$, depending on the value of $X_n$.  Thus, by the hypothesis on $f_{n-1}$, it induces a bijection
$$ \Big\{ (X_1, \ldots, X_n)\in \mathbb{N}^n \ | \ s=X_1+...+X_n \Big\} \xrightarrow{f_{n-1}} \Big[ 0, \binom{s+n-1}{n-1} -1\Big]  $$
defined by $(X_1, \ldots, X_n) \mapsto f_{n-1}(X_1, \ldots, X_{n-1})$.
Thus $f_n$ induces a bijection from the set on the left to the interval $\Big[\binom{s+n-1}{n}, \binom{s+n-1}{n} + \binom{s+n-1}{n-1}-1\Big]$.  Since $\binom{s+n-1}{n} + \binom{s+n-1}{n-1} = \binom{s+n}{n}$, the claim is proved.
The fact that $f_n$ is a bijection from $\mathbb{N}^n$ to $\mathbb{N}$ then follows immediately from the claim.
