Correctness of Euclid's Algorithm