a,b:
. 
y:. GCD(a;b;y)a,b,y:. GCD(a;b;y) 
GCD(a;-b;y)b:
, a:. y:. GCD(a;b;y)| Rank | Theorem | Name |
| 4 | a,b:. y:. GCD(a;b;y) | [gcd_exists] |
| cites the following: | ||
| 3 | a,b,y:. GCD(a;b;y) GCD(a;-b;y) | [gcd_p_neg_arg_2] |
| 2 | b:, a:. y:. GCD(a;b;y) | [gcd_exists_n] |