Integer Square Root Algorithm I'm currently working my way through David M. Bressoud's "Factorization and Primality Testing", and I'm struggling with an exercise (exercise 5.7) that asks the reader to prove that the following algorithm produces the greatest integer less than or equal to the square root of $n$:
\begin{align} 
\text{INITALIZE:} \quad &\text{READ} \;n \\ 
&a \leftarrow n \\ 
&b \leftarrow \lfloor (n+1)/2 \rfloor \\\\
\text{MYSTERY_LOOP:} \quad &\text{WHILE} \: b < a \; \text{DO} \\ 
&\quad a \leftarrow b \\
&\quad b \leftarrow \lfloor (a \times a + n) / (2 \times a) \rfloor \\\\
\text{TERMINATE:}\quad &\text{WRITE} \; a
\end{align} 
I know from real analysis that the sequence $x_{m+1} = \frac{x_m^2 + n}{2 x_m}$ converges to the square root of $n$ (for any sensible $x_0$), so morally, I can believe that the above algorithm converges to the integer square root of $n$.
How do we formally prove that the above algorithm works (i.e. terminates in a finite number of steps, such that $a^2 \leq n$ and $(a+1)^2 >n$), and moreover, why start the iterations with $b = \lfloor\frac{n+1}{2} \rfloor$? Is $\lfloor\frac{n+1}{2} \rfloor$ just a very crude approximation? What is its significance? 
I have tried splitting the floor into a real part minus a part between 0 and 1 (i.e. $\lfloor x \rfloor = x - \{x\}$), but I haven't been able to get very far with this. 
In addition, do we have the same quadratic convergence that we get when we compute the (ordinary) square root using Newton's method?

After some rooting around, I have found the answer on another thread, but for the sake of completeness, I will reproduce the argument here (the proof is taken from a textbook of Cohen):
First, note that $a$ and $b$ are always positive. If the algorithm did not terminate, then the condition in the mystery loop ($b <a$) implies that we'd have an infinite, strictly decreasing, sequence of positive integers, which is a contradiction, as there are only finitely many numbers less than $n$. So the algorithm terminates.
Hence, at some point, we must have that $b \geq a$, i.e. $$\left\lfloor \frac{a^2 +n}{2a} \right\rfloor \geq a.$$ Also note that $$\frac{t^2 + n}{2t} \geq \sqrt{n}$$ for all positive $t$ (easily shown), thus we have $$a \geq \left\lfloor\sqrt{n}\right\rfloor.$$ So assume $a$ does not equal $\lfloor\sqrt{n}\rfloor$. So $a \geq \lfloor\sqrt{n}\rfloor +1$ which implies that $a^2 > n$. Putting this together, we get $$0 \leq\left\lfloor\frac{a^2 +n}{2a}\right\rfloor -a = \left\lfloor \frac{n -a^2}{2a} \right\rfloor < 0$$ because $n-a^2 < 0$. This is a contradiction, and thus, $a$ must be equal to the integer square root of $n$. 
On the link above, there is also some discussion on the complexity of the above algorithm, which I may add in later.
