a:
, n:
, p,q:. Div(a;n;p) 
Div(a;n;q) p = qi,j,k:
. i
j j < k i < ka,b:, n:. n
a < nb a < b| Rank | Theorem | Name |
| 3 |
Thm* a:, n:, p,q:. Div(a;n;p) Div(a;n;q) p = q | [div_unique] |
| cites | ||
| 0 | Thm* i,j,k:. ij j < k i < k | [lt_transitivity_2] |
| 2 |
Thm* a,b:, n:. na < nb a < b | [mul_cancel_in_lt] |