Proof by induction that $x_{n} + by_{n} = a$ I have an algorithm where a and b $\in$ Z+
MUL(a,b)
   x = a
   y = 0
WHILE x >= b DO
   x = x-b
   y = y+1
IF x = 0 THEN
   RETURN(y)
ELSE
   RETURN(-1)

I need to prove by induction that 
$x_{n} + by_{n} = a$
is true if $x_{n}$ and $y_{n}$ are the values for x and y after n runs of the WHILE-loop.
My approach is to to prove that its true for the basecase where the WHILE-loop runs 0 times.
When the WHILE-loop runs 0 times (n = 0), we know that y = 0 since y is counting the amount of times the WHILE-loop is ran.
So we have:
\begin{equation}
\begin{split}
    x_{0} + by_{n} =& a \\
    x_{0} + b*0 =& a \\
    x_{0} =& a \\
\end{split}
\end{equation}
If we input $a = 1$ og $b = 2$ into $MUL()$. The result will be be $y = 0$ and $x = 1 = a$.
I'm not sure if this basecase step is correct and I am not sure how to proceed from here. I know I need to prove if it's true for n + 1. But how I do it I don't know. I hope somebody can help me!
 A: Strictly speaking, we do not know anything like "$y$ is counting the amount of times the WHILE loop is run" beforehand; however, this (i.e., $y_n=n$) may be a corollary of an analysis of the code.
After $0$ loops, i.e., immediately before entering the while loop, only x = a and y = 0 are executed, hence indeed $x_0=a$ and $y_0=0$. Thus 
$$\tag1 x_n+by_n=a\qquad\text{and}\qquad y_n=n$$
holds for the base case $n=0$
Assume $x_n+by_n=a$ and $y_n=n$ after $n$ loops. Then in the next loop, the statements x = x - b and y = y + 1 are executed. It follows that $x_{n+1}=x_n-b$ and $y_{n+1}=y_n+1$. Therefore, using the induction hypothesis, 
$$x_{n+1}+by_{n+1}=x_n-b+b(y_n+1)=x_n+by_n=a $$
and 
$$y_{n+1}=x_n+1=n+1,$$
i.e., $(1)$ with $n\leftarrow n+1$. Therefore we have shows that $(1)$ holds for all $n\in\Bbb N_0$.

Once this is shown, we see from $(1)$ that 
$$x_n=a-by_n=a-bn. $$
So for $n$ large enough, $x_n\ge b$ will not hold, and the WHILE loop will terminate.
Let $n$ be minimal with $x_n<b$. Then the return value of MUL will be $y_n$ if $x_n=0$, and $-1$ otherwise. As $x_n=0$ implies $by_n=a$, we conclude that for $a,b\in \Bbb Z^+$,
$$\text{MUL}(a,b)=\begin{cases}\frac ab&\text{if }b\text{ divides }a\\-1&\text{otherwise}\end{cases} $$
