1package Sqrt is 2 3 function Isqrt(N: Natural) return Natural; 4 --# return R => R * R <= N and (R + 1) * (R + 1) > N; 5 6end Sqrt; 7