Proof of Euclid's GCD Algorithm

In an advanced algorithms course I recently took the first algorithm covered, as I imagine is the case in many such courses, was Euclid's greatest common divisor method. Euclid's gcd is often considered the earliest known algorithm. Does that make Euclid the first programmer? (Note: Euclid's method, invented over 2000 years ago, is still very efficient even by today's standards and is enormously more powerful then the method you probably learned in middle school.) Euclid's gcd is based on the following observation:

gcd(m,n) = gcd(n, m mod n)

This equality is repetitively applied until a final condition, gcd(m,0), is reached for which case m is taken to be the gcd of m, n.

Now, although we weren't asked to prove this for my course, at the time I was inspired to attempt it. After lengthy pondering I wasn't able and eventually gave up disappointed. Recently I revisited the problem and was able to see the solution pretty quickly. I guess my math skills are improving (or so I like to think). Below is my proof. You will have to take my word for it that I didn't Google it (I didn't, I swear.)

Starting with the final condition, which is pretty trivial, if m mod n = 0 then by definition m is divisible by n so n is the gcd. Next we need to show that we get to that final condition, i.e. that we don't get stuck at m mod n != 0. Again, this is pretty simple. m mod n < n necessarily. Since we keep feeding m mod n into the procedure as the new n, n gets smaller each iteration. Since m mod 1 = 0 for all m, we must reach 0 eventually.

The hard part for me before was solving the general equality, gcd(m,n) = gcd(n, m mod n). I now find this pretty simple too and am even a bit embarrassed that I didn't come up with it before. Observe that if m and n are divisible by x then m-n is also divisible by x: (m-n)/x =(m/x)-(n/x). Likewise, m-an is also divisible by x for any a. Since the definition of m mod n is m-an for the largest a where m-an>0 it follows that any common divisor of m and n is also a common divisor of m mod n. So if x is the gcd for m and n, it is also the gcd of m mod n (since m mod n is necessarily smaller than both m and n).

QED

If any reader sees a flaw in my reasoning, please reply. I really want to be sure of this.