Abstract
This is a formalisation of the proof of an inequality by Trevor D. Wooley attesting that when
$\lambda > 0$, $$\min_{r \in \mathbb{N}}(r + \lambda/r) \leq \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.