Since
\begin{equation}
\left( \frac{c}{4} \right)^2
= \left( \frac{2 a + 2 b}{2 \cdot 2} \right)^2
= \left( \frac{a + b}{2} \right)^2
\end{equation}
then this result is a special case of
R5210: Tight upper bound to a product of two unsigned real numbers. $\square$
