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