a:
, n:
. a
n 
(a 
n) = ((a-n) n)+1a:, n:. 
q:. Div(a;n;q) & (a n) = qa,b,n:
. a
b 
a+nb+na:, n:, p,q:. Div(a;n;p) Div(a;n;q) p = qa,b,n:. a+nb+n aba,b,n:. a+n < b+n a < b| Rank | Theorem | Name |
| 7 |
Thm* a:, n:. an (a n) = ((a-n) n)+1 | [div_rec_case] |
| cites | ||
| 6 |
Thm* a:, n:. q:. Div(a;n;q) & (a n) = q | [div_elim] |
| 3 |
Thm* a,b,n:. ab a+nb+n | [add_mono_wrt_le_rw] |
| 3 |
Thm* a:, n:, p,q:. Div(a;n;p) Div(a;n;q) p = q | [div_unique] |
| 1 |
Thm* a,b,n:. a+nb+n ab | [add_cancel_in_le] |
| 2 |
Thm* a,b,n:. a+n < b+n a < b | [add_cancel_in_lt] |