a,b:
. CoPrime(a,b) 
(
x,y:. a
x+by = 1)a,b:. CoPrime(a,b) (x,y:. (ax+by) ~ 1)a,b:. (a ~ b) 
a = b 
a = -bi,j:. i = j -i = -j| Rank | Theorem | Name |
| 6 | a,b:. CoPrime(a,b) (x,y:. ax+by = 1) | [coprime_bezout_id1] |
| cites the following: | ||
| 4 | a,b:. CoPrime(a,b) (x,y:. (ax+by) ~ 1) | [coprime_bezout_id0] |
| 5 | a,b:. (a ~ b) a = b a = -b | [assoced_elim] |
| 0 | i,j:. i = j -i = -j | [minus_functionality_wrt_eq] |