a:
, n:
. (a 
n) 
i,j:
. i
j 
i < j+1a,b:, n:. n
a < nb 
a < ba:, n:
. a = (a n)n+(a rem n)i1,i2,j1,j2:. i1 < j1 i2j2 i1+i2 < j1+j2a:, n:. 0(a rem n) & (a rem n) < n| Rank | Theorem | Name |
| 3 |
Thm* a:, n:. (a n) | [divide_wf] |
| cites | ||
| 0 | Thm* i,j:. ij i < j+1 | [le_to_lt] |
| 2 |
Thm* a,b:, n:. na < nb a < b | [mul_cancel_in_lt] |
| 0 |
Thm* a:, n:. a = (a n)n+(a rem n) | [div_rem_sum] |
| 1 |
Thm* i1,i2,j1,j2:. i1 < j1 i2j2 i1+i2 < j1+j2 | [add_functionality_wrt_lt] |
| 0 |
Thm* a:, n:. 0(a rem n) & (a rem n) < n | [rem_bounds_1] |