a,b:
. (
x,y:. a
x+by = 1) 
CoPrime(a,b)a:. 1 | aa,b,c:. a | b a | bca,b1,b2:. a | b1 a | b2 a | b1+b2| Theorem | Name |
| a,b:. (x,y:. ax+by = 1) CoPrime(a,b) | [coprime_bezout_id2] |
| cites the following: | |
| a:. 1 | a | [one_divs_any] |
| a,b,c:. a | b a | bc | [divisor_of_mul] |
| a,b1,b2:. a | b1 a | b2 a | b1+b2 | [divisor_of_sum] |