b:
. b | 1 
prime(b)y:. prime(-y) 
prime(y)a,b:. a | b -a | bb:
. b | 1 prime(b)| Rank | Theorem | Name |
| 12 | b:. b | 1 prime(b) | [no_prime_divs_one] |
| cites the following: | ||
| 3 | y:. prime(-y) prime(y) | [prime_neg] |
| 0 | a,b:. a | b -a | b | [divides_invar_1] |
| 11 | b:. b | 1 prime(b) | [no_nat_prime_divs_one] |