Implement a gcd(x, y) Function

[wdcraft01]

trafficstars

Implement a positive integer-valued greatest common divisor function, gcd(x, y), to represent the greatest common divisor of two integer inputs x and y. Notice that we have the following properties: (1) gcd(x, 0) = abs(x) (2) gcd(x, x) = abs(x) (3) gcd(0, 0) = 0 (although this is sometimes left undefined) (4) gcd(1, x) = abs(x) A gcd() function has already been partially defined in the proving_sqrt_2 branch in the proveit/number/ directory in GCD.py, in part to implement the sqrt(2)-not-rational proof.