a:
, b:
. a | b & 
b | a 
a<b & a | ba:, b:. a | b 
a
ba,b:. (a ~ b) a = b| Rank | Theorem | Name |
| 7 | a:, b:. a | b & b | a a<b & a | b | [pdivisor_bound] |
| cites the following: | ||
| 1 | a:, b:. a | b ab | [divisor_bound] |
| 6 | a,b:. (a ~ b) a = b | [assoced_nelim] |