I have an interesting puzzle: Given two non-negative integers, let's call them $x$ and $y$, work out a formula for $z$ as shown in the table below:
x
___|_0__1__2__3__4_...
0 | 0 1 3 6 10
1 | 2 4 7 11 16
y 2 | 5 8 12 17 23 ...
3 | 9 13 18 24 31
4 |14 19 25 32 40
...|20 26 33 41 50
...
where $z$ is the number in the middle. You should see a pattern if you look along the (positive) diagonals. This question is about the next part of this puzzle, so I will show a basic formula for $z$ below. If you want to solve this yourself, look away now. Seriously, I think you should try solving it yourself. As you're still reading, here's the formula:
$$\frac{(x+y)(x+y+1)}{2}+y = z$$
When $y = 0$, $z$ is the $x$th triangular number. Following a line down and to the left shows a similar number, just incremented by one. So what if we tried the $x+y$th triangular number? It's close, but we still need it increasing by one as it goes down. So we add $y$ onto the $x+y$th triangular number, giving the result.
Knowing that $x$, $y$ and $z$ will always be non-negative integers, and knowing that for each unique $x$ and $y$, there is only one $z$, and that for each unique $z$, there is only one pair of $x$ and $y$, surely it's possible to calculate $x$ and $y$ given only $z$.
That is, to create a formula for $x$ in terms of $z$, and to create a formula for $y$ in terms of $z$. I know it's possible, and I've tried it, but I keep hitting things that I don't know how to do. So I thought I'd publish the problem, and learn from it at the same time.
Please answer with an explanation.

This is a variant of the Cantor diagonalization.
See Cantor pairing function for more information.
Cantor used it to show that $\mathbb{N}^2$ has the same cardinality as $\mathbb{N}$.
In theoretical computer science it is used to show that register machines with $n$ arguments can be modeled by register machines with one argument, by iteratively encoding and decoding the $n$ arguments into one argument.