a:
, n:
. Div(a;n;a 
n)a:, n:. 0
(a rem n) & (a rem n) < na,b,n:
. ab 
a+nb+na,b,n:. a < b a+n < b+na:, n:
. a = (a n)
n+(a rem n)a,b:. a+b = b+a| Rank | Theorem | Name |
| 5 |
Thm* a:, n:. Div(a;n;a n) | [div_fun_sat_div_nrel] |
| cites | ||
| 0 |
Thm* a:, n:. 0(a rem n) & (a rem n) < n | [rem_bounds_1] |
| 3 |
Thm* a,b,n:. ab a+nb+n | [add_mono_wrt_le_rw] |
| 4 |
Thm* a,b,n:. a < b a+n < b+n | [add_mono_wrt_lt_rw] |
| 0 |
Thm* a:, n:. a = (a n)n+(a rem n) | [div_rem_sum] |
| 0 | Thm* a,b:. a+b = b+a | [add_com] |