a,b:
, n:
. n
a
nb 
aba,b:, n:. na < nb a < ba,b:, n:
. na = nb a = b| Rank | Theorem | Name |
| 4 |
Thm* a,b:, n:. nanb ab | [mul_cancel_in_le] |
| cites | ||
| 2 |
Thm* a,b:, n:. na < nb a < b | [mul_cancel_in_lt] |
| 3 |
Thm* a,b:, n:. na = nb a = b | [mul_cancel_in_eq] |