a,b:
. 
u,v:. GCD(a;b;u
a+vb)b:
, a:. u,v:. GCD(a;b;ua+vb)a,b,y:. GCD(a;b;y) 
GCD(a;-b;y)| Rank | Theorem | Name |
| 3 | a,b:. u,v:. GCD(a;b;ua+vb) | [bezout_ident] |
| cites the following: | ||
| 2 | b:, a:. u,v:. GCD(a;b;ua+vb) | [bezout_ident_n] |
| 2 | a,b,y:. GCD(a;b;y) GCD(a;-b;y) | [gcd_p_neg_arg] |