Relating a proof to a Haskell program
Your goal is to “prove”  --I'm using bullets “•” for syntactic separators--
$$ ∀x \;•\;\; ∃y \;•\;\; y² ≤ x &lt; (y+1)²$$



Proof Methods

In the natural deduction style, one proves “∀ x : ℕ • P x” by proving
two statements: 

Base case      :: P 0
Inductive step :: P a ⇒ P (S a) , for a : ℕ and S successor function


Where, in this case,
$$P x \;\;≡\;\; ∃y \;•\; y² ≤ x &lt; (y+1)²$$

In the constructive fashion, one proves “∃ y • Q x” by 
actually finding such a $y$ using whatever data is available.

Base case

For the [base] case the input x is 0, and we need to find
some $y$ with $y² ≤ x &lt; (y+1)²$. Clearly $y = 0$ works as shown
in the proof your posted.

Inductive step

For the [inductive] case where the input x is of the shape S a,
we need to find a $y$ with $y² ≤ S a &lt; (y+1)²$, (*).


However, we have the assumption $P a$ which gives us a $b$ with
$b² ≤ a &lt; (b+1)²$ --which looks really close to the goal (*).
To reach our goal (*), let's do the simplest thing possible:
replace $a$ with $S a$ in (1) thereby obtaining
$b² ≤ S a &lt; (b + 1)²$. Because of (1), and the transitivity of ≤,
the left part is true and the whole thing reduces to:
$$S a &lt; (b + 1)²$$
So if this is true, then we are done and the answer is $b$.
If it is not true, then we must have it complement:
$$(b + 1)² ≤ S a$$


But from (1) we also have $a &lt; (b + 1)² = b² + 2b + 1$
thus we obtain $S a = a + 1 &lt; (b² + 2b + 1) + 1 ≤ b² + 4b + 2 = ((b + 1) + 1)²$
Hence, we have found that $(b + 1)² ≤ S a &lt; ((b + 1) + 1)²$
and so we may take the output $y$ to be $b + 1$ for our goal (*).





Curry-Howard: Proving ≅ Programming

The above was a proof [sketch] which corresponds to the a program.

A proof of $$∀ x : ℕ • ∃ y : ℕ • R(x, y)$$
corresponds to the program

-- Output y = prog x satisfies relationship R(x, y), for all input x.
prog :: Int → Int
prog 0  = “the y found in the base case of the proof”
prog n  = “the y found in the inductive step, 
             along with any conditionals and recursive calls”


Applying this to our above proof yields,

prog :: Int → Int
prog 0 = 0
prog n = let a = n - 1 ; b = prog a
         in
           if   a + 1 &lt;= (b + 1) * (b + 1)
           then b
           else b + 1


Hope that helps :-)