a,b:
. CoPrime(a,b) 
(
x,y:. (a
x+by) ~ 1)a,b:. u,v:. GCD(a;b;ua+vb)a,b,y:. GCD(a;b;y) GCD(b;a;y)a,b,y1,y2:. GCD(a;b;y1) GCD(a;b;y2) (y1 ~ y2)| Rank | Theorem | Name |
| 4 | a,b:. CoPrime(a,b) (x,y:. (ax+by) ~ 1) | [coprime_bezout_id0] |
| cites the following: | ||
| 3 | a,b:. u,v:. GCD(a;b;ua+vb) | [bezout_ident] |
| 0 | a,b,y:. GCD(a;b;y) GCD(b;a;y) | [gcd_p_sym] |
| 0 | a,b,y1,y2:. GCD(a;b;y1) GCD(a;b;y2) (y1 ~ y2) | [gcd_unique] |