Solution (source code)

= Solution
{c}

The tail $(a_n)_{n\geq1}$ is a <monotone sequence> bounded below by zero. The <bounded monotone sequence theorem> therefore gives $a_n\to L\geq0$. Taking the <limit of a sequence> in $a_n^2\geq c$ yields $L^2\geq c>0$, so $L>0$. The reciprocal rule from part (a) permits passage to the <limit of a sequence> in the <recurrence relation>:
$$
L=\frac12\left(L+\frac cL\right).
$$
Multiplication by $2L$ gives
$$
\boxed{L>0,\qquad L^2=c.}
$$
This proves existence of the positive <square root> without assuming that existence when constructing the <sequence>.