# Computing square roots (with well-founded recursion)

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 that uses this algorithm to
compute the square root and is based on well-founded recursion. This
function should have 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: Mon Mar 1 11:29:21 MET 2004