GCD code in plain old C, and a correctness question