A Recursively Defined Square-Root Sequence

In the setting of The Real Line: Standing Notation and Background for Calculus, with the square root $\sqrt{\alpha}$ of a nonnegative real number $\alpha$ as fixed there, define a sequence of real numbers $(a_n)_{n\in\mathbb{N}}$ by

This recursion is legitimate: $0\le a_1$, and whenever $0\le a_n$ we have $0\le 2+a_n$, so $a_{n+1}$ is defined and satisfies $0\le a_{n+1}$; the principle of induction then gives a well-defined sequence with $0\le a_n$ for every $n\in\mathbb{N}$.

Problem. Show that

that $(a_n)$ converges, and that