# Computing square roots

Given a natural number *x*, we want to compute the pair of numbers
*s* and *r* such that *s * s ≤ x < (S+1)*(s+1)*
and *x=s*s+r*.

. Let *x=4*q+r0* with *r<4*. If *s'*
and *r'* are the result for computing the square root of *q*, then there
are two possibilities:
- If
*4*r'+r0 <4*s'+1* then
either *s=2s'* and *r=4r'+r0*
- Otherwise
*s=2s'+1* and *r=r4'+r0-4s'-1*

Build a function with bounded recursion that uses this algorithme to
compute the square root. Prove that it is correct and then use it
to obtain a function with the following type:
sqrt_nat : forall n:nat,
{s : nat & {r : nat | n = s * s + r /\ n < (s + 1) * (s + 1)}}

## Solution

Follow this link

Going home

Yves Bertot
Last modified: Tue May 20 15:26:16 MEST 2003