a,p:
. prime(p) 
(CoPrime(p,a) 
p | a)a,b:. CoPrime(a,b) (c:. c | a c | b (c ~ 1))a,b:. (c:. c | a c | b c | 1) CoPrime(a,b)p:. prime(p) p = 0 & (p ~ 1) & (a:. a | p (a ~ 1) 
(a ~ p))| Rank | Theorem | Name |
| 10 | a,p:. prime(p) (CoPrime(p,a) p | a) | [coprime_iff_ndivides] |
| cites the following: | ||
| 1 | a,b:. CoPrime(a,b) (c:. c | a c | b (c ~ 1)) | [coprime_elim] |
| 1 | a,b:. (c:. c | a c | b c | 1) CoPrime(a,b) | [coprime_intro] |
| 9 | p:. prime(p) p = 0 & (p ~ 1) & (a:. a | p (a ~ 1) (a ~ p)) | [prime_elim] |