a:
, n:
, k:. k
(a 
n) 
k
naa:, n:. 
q:. Div(a;n;q) & (a n) = qa,b:
, n:. ab 
nanbi,j,k:. ij j < k i < ka,b:. ab = baa,b:, n:. na < nb a < b| Rank | Theorem | Name |
| 7 |
Thm* a:, n:, k:. k(a n) kna | [div_lbound_1] |
| cites | ||
| 6 |
Thm* a:, n:. q:. Div(a;n;q) & (a n) = q | [div_elim] |
| 1 |
Thm* a,b:, n:. ab nanb | [mul_preserves_le] |
| 0 | Thm* i,j,k:. ij j < k i < k | [lt_transitivity_2] |
| 0 | Thm* a,b:. ab = ba | [mul_com] |
| 2 |
Thm* a,b:, n:. na < nb a < b | [mul_cancel_in_lt] |