Proving GCD algorithm terminates I'm reading this article on a GCD algorithm described by Dijkstra:
https://www.cs.utexas.edu/users/EWD/transcriptions/EWD03xx/EWD316.4.html

I'm looking at program 1.  In particular I'm trying to understand the proof that the loop terminates.  Here is program 1 (my notation is slightly different than the one in the article):

function GCD(a,b) 

while a != b
    if a &gt; b 
        a = a - b
    else
        b = b - a

return a


I get that max(a,b) at loop n is strictly greater than max(a,b) at loop n+1.  Since a and b are integers greater than 0 it follows that max(a,b) is always greater than 0.  This implies a lower bound.  Therefore the while loop must terminate.  

Is my understanding correct?
If you just care about termination of the algorithm not the tight analysis then you can say that it will terminates within $a+b$ steps as inside the while loop you are decreasing either $a$ or $b$ depending on some condition, so your while loop have to terminate within $a+b$ iterations.