gcd(x, y) = gcd(x % y, y)
Proof:
d = gcd(x, y)
⇒ (d | x) ^ (d | y) ^ (d - max divisor)
⇒ (x = d*$k_{1}$) ^ (y = d*$k_{2}$)
x - y = d*$k_{1}$ - d*$k_{2}$ = d($k_{1}$ - $k_{2}$)
⇒ d | (x - y) ⇒ gcd(x, y) = gcd(x - y, y)
gcd(x, y) = gcd(x - y, y) = gcd(x - 2y, y) = gcd(x - 3y, y) = … = gcd(x % y, y)
gcd(x, y) = gcd(x % y, y) → gcd(y, x % y) → gcd(y % (x % y), x % y) → … reducing both arguments by at least 1 bit … → gcd(0, x) → return x