Theorem. Euclid [004Z]

The euclidean algorithm computes the greatest common divisor.

Proof. TODO