Prove correctness of iterative LCM algorithm I have been trying to prove the following algorithm, without success. 

Here is the C-Style pseudocode:

//j,k &gt;= 0
int get_lcm(int j, int k){
    int c = j;
    int d = k;
    while(c != d){
        if(c &lt; d){
            c += j;
        } else {
            d += k;
        }
    }
    return c;
}


I tried to find the loop invariant, which ended up being something like:
$$
\begin{aligned}
&amp;c\le\text{LCM}(j,k) \wedge d\le\text{LCM}(j,k) \wedge c=aj \wedge d =bk\\
&amp;(a,b \in N)
\end{aligned}
$$
I'm not sure how to proceed from here. I understand intuitively why the algorithm works, but I'm having trouble putting out an actual formal proof of it. 

I need to come up with an invariant such that $c=d=LCM(j,k)$ when $c=d$. I'm having trouble showing how $c, d \le LCM(j,k)$ after one iteration.

Can anybody please help me? Thank you for your time.
Assume j, k > 0. 

You have your loop invariant. Every iteration, one of c or d gets larger. They cannot forever stay ≤ LCM (i, j), therefore the loop must finish. 

Because c and d are multiples of i, j, they cannot change directly from being &lt; LCM (i, j) to > LCM (i, j), instead there must be a step for each of c and d where it is equal. 

If both are = LCM (i, j) then c = d and the algorithm exits. If one is = LCM (i, j) then the other one is smaller and gets increased.