I am trying to relate the following integer square root theorem

$\forall x: \mathbb{N}, \exists y : \mathbb{N}((y^2 \leq x) \land (x < (y+1)^2))$

and its proof to its role as a specification of the Integer Square Root isqrt ($\lfloor \sqrt{x} \rfloor$) function in a Haskell program.

Below is a inductive proof of the theorem and the related Haskell program. The proof was done using the Fitch system, hence there are notational differences between code and proof e.g. no $\leq$ in Fitch.

For my question the details of the proof are not important. I wish to focus on the base case, and the two cases involving $\exists$-Elimination and $\lor$-Elimination.

I used Quickcheck as a reasonable check that the theorem holds in the code.

I can see that cases 1 and 2 in the proof correspond to the guard conditions in the Haskell definition of isqrt function. I did not specify, prove, and implement the function isqrt in any structured way. I just used any examples I could find. I believe that there must some more formal transformation from proof to code that I am missing. So despite having written both the proof and code the precise correspondence between both eludes my comprehension.

module Peano where
import Test.QuickCheck

data Nat = Z | S Nat deriving Show

(+@) :: Nat -> Nat -> Nat
Z +@ y = y
(S x) +@ y = S (x +@ y)

(*@) :: Nat -> Nat -> Nat
x *@ Z = Z 
x *@ S y = (x *@ y) +@ x 

sqr x = x *@ x 

(=@) :: Nat -> Nat -> Bool
Z =@ Z  = True
(S m) =@  (S n) = m =@ n 
_=@ _  = False 


(<@) :: Nat -> Nat -> Bool
Z <@ Z = False 
Z <@ x | not(x =@ Z) = True 
x <@ Z | not(x =@ Z) = False 
(S x) <@ (S y) = x <@ y 



(<=@) :: Nat -> Nat -> Bool
x <=@ y = if (x =@ y) || (x <@ y) then True else False



isqrt Z = Z
isqrt (S x) | (sqr (S (isqrt x))) <=@  (S x) = (S (isqrt x))
            | (S x) <@ (sqr (S (isqrt x))) = isqrt x


instance Arbitrary Nat where
 arbitrary = oneof [return Z, (S  <$>  arbitrary) ]

isqrtPostCondition :: Nat  -> Bool
isqrtPostCondition x  = (sqr (isqrt x) <=@ x) && (x <@ sqr(S (isqrt x)))
check = quickCheck isqrtPostCondition