I would like to use Lambek-Moser theorem. While part of the work is hidden in the proof of the theorem, note that the proof is not difficult. It can be a high-school exercise. My main purpose is to highlight the part of the work that is a pure recipe for problems like this. Namely, we have an increasing function enumerating a subset of the natural numbers and we want to produce an enumeration for the complement.
Definition:
Call a pair of non-increasing function $f,g:\mathbb{N}\to\mathbb{N}$ a Galois connection when
$$f(m)\leq n\iff m\leq g(n)$$
They are like "inverses of each other with respect to inequalities".
Observation:
$$
\begin{align}
f(m)&=\min\{n:\ m\leq g(n)\}\\
g(n)&=\max\{m:\ f(m)\leq n\}
\end{align}
$$
Lambek-Moser theorem: $f,g:\mathbb{N}\to\mathbb{N}$ are a Galois connection if and only if
$$
\begin{align}
A&=\{f(m)+m:\ m\in\mathbb{N}\}\\
B&=\{g(n)+n+1:\ n\in\mathbb{N}\}
\end{align}
$$
partition $\mathbb{N}$.
Let $F(m)=m^2$. We would like to find increasing $G(n)$ such that their ranges partition $\mathbb{N}$. So, define $f(m)=F(m)-m=m^2-m$. The pronic numbers. We just need to compute the "inequality inverse" $g$ of $f$, and that would give $G(n)=g(n)+n+1$, by Lambek-Moser. Already the observation is giving an explicit formula
$$G(n)=\max\{m:\ f(m)\leq n\}+n+1$$
which can be made more explicit, by solving the inequality
$$m^2-m=f(m)\leq n$$
This is quadratic with solution
$$\frac{-\sqrt{4 n + 1} + 1}{2}\leq m\leq\frac{\sqrt{4 n + 1} + 1}{2}$$
So, $g(n)=\left\lfloor\frac{\sqrt{4 n + 1} + 1}{2}\right\rfloor$ and
$$G(n)=\left\lfloor\frac{\sqrt{4 n + 1} + 1}{2}\right\rfloor+n+1=\left\lfloor\sqrt{n+1/4}+1/2\right\rfloor+n+1$$
Recall that $\lfloor x+1/2\rfloor$ gives the closest integer (rounding up in the equal distance case), and that here we count starting from $n=0$, while in your case you start from $n=1$, and you get your formula.
