a,b:
, n:
. n
a
nb 
aba,b:
, n:. nanb 
abi1,i2,j1,j2:. i1j1 i2j2 i1i2j1j2| Rank | Theorem | Name |
| 3 | a,b:, n:. nanb ab | [nat_factor_cancel_rw] |
| cites the following: | ||
| 2 | a,b:, n:. nanb ab | [mul_cancel_in_le] |
| 1 | i1,i2,j1,j2:. i1j1 i2j2 i1i2j1j2 | [multiply_functionality_wrt_le] |