Introduction
In computer science there is a field called Formal Methods and Specifications. In this field software designers design softwares by specifying their functionalities in formal methods, for example in set theory.
Problem
In this field a program that calculates square root of a number is specified by
\begin{align} \forall a \in \mathbb{N} \cdot \exists b \in \mathbb{N} \cdot (b \times b \le a) \land (a < (b+1) \times (b+1)) \end{align}
where in this formula, a is program's input and b is program's output. Now I want to prove this statement by induction on a. As such, I should show that this statement is true for a = 0 and if this is true for a = x, I should prove that this is also true for a = x + 1.
Also proofs other than Induction is also okay.
For induction, I do not know how should I prove this statement for a = x + 1 when this statements holds for a = x
For the induction step, you assume that $a \in \mathbb{N}$ and that $$\exists b \in \mathbb{N} . (b \times b \le a) \land (a < (b+1) \times (b+1)). \tag{1}$$
Now, depending on exactly how your formal system is formulated, there should be some way to identify a witness for $(1)$, that is, for the inductive step you can introduce a free variable $b_0$ and assume that $(b_0 \times b_0 \le a) \land (a < (b_0+1) \times (b_0+1)).$
For $a + 1$, then, there are two cases. In one case, $a + 1 < (b_0 + 1) \times (b_0 + 1).$ You can then prove (via some additional formal steps) that $(b_0 \times b_0 \le a + 1)$, and therefore that $$\exists b \in \mathbb{N} . (b \times b \le a+1) \land (a+1 < (b+1) \times (b+1)).$$
In the other case, $a + 1 \geq (b_0 + 1) \times (b_0 + 1).$ If you can then prove (via additional formal steps) that $(a < ((b_0+1)+1) \times ((b_0+1)+1)),$ these two inequalities establish that $$\exists b \in \mathbb{N} . (b \times b \le a + 1) \land (a + 1 < (b+1) \times (b+1)), \tag{2}$$ using $b_0 + 1$ as a witness for $b$.
You then need at least one more formal step in order to combine the conclusions of the two cases so that you can state formula $(2)$ outside the context of either case, that is, in a context where you have assumed only $a \in \mathbb N$ and formula $(1)$, to complete the inductive step.
This is merely a strategy for the proof. Obviously you will need to produce a sequence of formal inferences; the details depend on exactly what inferential tools you are allowed to use and on the way in which they have been formulated.