b:
. b | 1 
b = 1a,b:. a | b 
(
c:. b = a
c)x,y:. xy = 1 x = 1 & y = 1| Rank | Theorem | Name |
| 4 | b:. b | 1 b = 1 | [only_one_nat_divs_one] |
| cites the following: | ||
| 2 | a,b:. a | b (c:. b = ac) | [divides_def_on_nat] |
| 3 | x,y:. xy = 1 x = 1 & y = 1 | [nat_prod_one_iff_factors_one] |