Computing square roots

Construct a (non-naïve) function that satisfies the following specification:

forall p:positive, 
  {s:Z &{r:Z | Zpos p = s*s+r /\ s*s <= Zpos p < (s+1)*(s+1)}}

Solution

Look at this file