a,b1,b2:
. CoPrime(a,b1) 
CoPrime(a,b2) CoPrime(a,b1
b2)a,b:. CoPrime(a,b) 
(
x,y:. ax+by = 1)a,b,n:. a = b a+n = b+ni1,i2,j1,j2:. i1 = j1 i2 = j2 i1i2 = j1j2| Rank | Theorem | Name |
| 8 | a,b1,b2:. CoPrime(a,b1) CoPrime(a,b2) CoPrime(a,b1b2) | [coprime_prod] |
| cites the following: | ||
| 7 | a,b:. CoPrime(a,b) (x,y:. ax+by = 1) | [coprime_bezout_id] |
| 0 | a,b,n:. a = b a+n = b+n | [add_mono_wrt_eq] |
| 0 | i1,i2,j1,j2:. i1 = j1 i2 = j2 i1i2 = j1j2 | [mul_functionality_wrt_eq] |