Sqrt(x) function implementation; what is $(i^2 \leq x) \land ((i + 1)^2 > x)$ checking?
I'll put the two inequalities together, for readability: $i^2 \leq x &lt; (i+1)^2$.

Taking the positive square of a positive number is a monotone function. Hence,
$$i^2 \leq x &lt; (i+1)^2 \implies i \leq |\sqrt{x}| &lt; i +1$$

Then, the interger part of $|\sqrt{x}|$ is obviously $i$.