Wooley's Discrete Inequality

This is a formalisation of the proof of an inequality by Trevor D. Wooley attesting that when $\lambda >0$, $$\underset{r\in \mathbb{N}}{min}(r+\lambda /r)\le \sqrt{4\lambda +1}$$ with equality if and only if $\lambda =m(m-1)$ for some positive integer $m$. The source is the note An Elementary Discrete Inequality by T. D. Wooley.