a1,a2,b:
. CoPrime(a1,a2) 
a1 | b a2 | b a1
a2 | ba,b:. CoPrime(a,b) 
(
x,y:. ax+by = 1)a,b,n:. a = b na = nb| Rank | Theorem | Name |
| 8 | a1,a2,b:. CoPrime(a1,a2) a1 | b a2 | b a1a2 | b | [coprime_divisors_prod] |
| cites the following: | ||
| 7 | a,b:. CoPrime(a,b) (x,y:. ax+by = 1) | [coprime_bezout_id] |
| 0 | a,b,n:. a = b na = nb | [mul_preserves_eq] |