I am trying to relate the following [integer square root theorem][1] 

$\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][2] of the theorem and the related Haskell program. 
The proof was done using the [Fitch system][3], 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 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. 
 
[![Inductive Proof][4]][4]

    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


  [1]: http://www.nuprl.org/MathLibrary/integer_sqrt/
  [2]: https://math.stackexchange.com/questions/2891932/inductive-proof-using-fitch-software
  [3]: https://www.press.uchicago.edu/ucp/books/book/distributed/L/bo12734345.html
  [4]: https://i.sstatic.net/Qr4Jp.png