I have a multivariate function:
$$ f(v_1, v_2)_\phi = v_1 \left(\phi - \frac{v_1 + 1}{2} - 1\right) + v_2 - 1 $$
Where $\phi \in \mathbb{N} $ is an argument of the function and $v_1, v_2 \in \mathbb{Z}$ such that $0 \leq v_1 < v_2 < \phi$. The expected codomain of the function is the set:
$$ \left\{0, 1, 2, \dots, \frac{(\phi - 1)\phi}{2} - 1 \right\} $$
I would like to prove that the function $f$ is bijective.
While I can prove bijection for single variable functions, I wasn't able to prove it in multiple variables. Experimental data suggest that it is indeed bijective.