b:
, a:
. 
u,v:. GCD(a;b;u
a+vb)a:. GCD(a;0;a)a:, b:
. q:, r:b. a = qb+ra,b,y:. GCD(a;b;y) 
GCD(b;a;y)a,b,y,k:. GCD(a;b;y) GCD(a;b+ka;y)a,b:. ab = ba| Rank | Theorem | Name |
| 2 | b:, a:. u,v:. GCD(a;b;ua+vb) | [bezout_ident_n] |
| cites the following: | ||
| 1 | a:. GCD(a;0;a) | [gcd_p_zero] |
| 1 | a:, b:. q:, r:b. a = qb+r | [quot_rem_exists] |
| 0 | a,b,y:. GCD(a;b;y) GCD(b;a;y) | [gcd_p_sym] |
| 1 | a,b,y,k:. GCD(a;b;y) GCD(a;b+ka;y) | [gcd_p_shift] |
| 0 | a,b:. ab = ba | [mul_com] |