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)}}