Prove correctness for this lcm iterative program Studying for finals, trying to solve this problem:

Given positive integers $n$ and $m$, we say that $m$ is a multiple of $n$ iff there is some $k \in N$ such that $m = kn$. 
For positive integers $a$, $b$, we define the least common multiple of $a$ and $b$, denoted $lcm(a, b)$, to be the smallest number that is both a multiple of $a$ and a multiple of $b$.
Prove that the following program is correct with respect to its given specification.
Precondition: $a$ and $b$ are positive integers. 
Postcondition: Return $lcm(a, b)$.

lcm(a, b)
x=a; y=b 
while x \= y:
    if x < y: 
        x=x+a
    else: 
        y=y+b
return x

My loop invariant so far:
For $k \in N$, define $P(k)$ as such:
$P(k)$: if $a$, $b$ are positive integers and the loop iterates at least $k$ times, then:


*

*$x_k \ge a$ and $y_k \ge b$

*$x_k$ is a multiple of $a$ and $y_k$ is a multiple of $b$

*$x_k \le ab$


I'm not sure if my LI is correct. I'm having a hard time proving the last one (#3) in my induction step and not really sure how to prove partial correctness either (I'm taking the approach of LI + exit condition implies post condition).
Any suggestions please?
 A: For $a,b > 1$, we know that $a,b < ab$. Your algorithm adds positive number to either $x$ or $y$, in each step. That means that in each step exactly one of this values grows, so - at one point - you'll get one of these:


*

*$x \ge ab$, $y < ab$; or

*$x < ab$, $y \ge ab$; or

*$x = y$.


Since you worry about $\le ab$, let us assume 1: $x \ge ab$, $y < ab$. Notice that $x = ab$. If this wasn't the case, we'd have $x - b \ge ab$, so the last step wouldn't enlarge $x$ and its value wouldn't get $>ab$, which is a contradiction.
So, $x = ab$, $y < ab = x$.
As long as $y < x$, the algorithm will keep on adding $b$ to $y$. So, your $y$ will be getting values $y_0, y_0 + b, \dots, y_0 + kb$ for some $k \in \mathbb{N}$ ($y_0$ denotes the value that $y$ had when $x$ reached $ab$).
Now, same as with $x$: if $y_0 + kb > ab$, then $y_0 + (k-1)b \ge ab$, because there are no numbers between $y_0 + (k-1)b$ and $y_0 + kb$ that are divisible by $b$. But, we know that $(k-1)b < ab$, so this is a contradiction. Hence, $y_0 + kb = ab = x$ and the algorithm ends.
The same goes for case 2, and the case 3 says only that the algorithm may finish sooner.
You still need to show that the value that the algorithm computes is the least (common multiplier). This can be done by repeating what I did above, but using $m = \operatorname{lcm}(a,b)$ instead of $ab$, thus showing that $x$ and $y$ cannot grow beyond it.
