Proof of correctness of algorithm Can someone help me prove the correctness of this algorithm:

MUL(a,b)
   x=a
   y=b
   WHILE x≥b DO
      x=x-b
      y=y+1
   IF x=0 THEN
      RETURN(true)
   ELSE
      RETURN(false)


I had to prove that $x_n + b\cdot y_n = a$ by induction, where $x_n$ and $y_n$ are the values of the variable x and y after the loop has iterated n times. 

I have done that, but I am not sure how to prove the correctness of the algorithm.
To prove that the algorithm is correct, we assume that the loop invariant  $x_n + by_n = a$  is true per induction.

we have the following two cases:

case 1:

If MUL(a,b) returns true, then $x_n = 0$ and $y_n = n$,

so 

$x_n + by_n =a \rightarrow bn = a \rightarrow a$ is a multiplum of b

case 2:

if MUL(a,b) returns false, then $x_n \not= 0$, so we have

$x_n + by_n = a \rightarrow bn \not= a \rightarrow a$ is not a divisor of b.