i,j:
, n:
. (((i rem n)+(j rem n)) rem n) = ((i+j) rem n)a:
, n:
. a = (a 
n)
n+(a rem n)a,b:, n:. ((a+bn) rem n) = (a rem n)a:, n:. 0
(a rem n) & (a rem n) < na:, n:. 0(a n)i1,i2,j1,j2:. i1j1 
i2j2 i1+i2j1+j2| Rank | Theorem | Name |
| 10 |
Thm* i,j:, n:. (((i rem n)+(j rem n)) rem n) = ((i+j) rem n) | [rem_addition] |
| cites | ||
| 0 |
Thm* a:, n:. a = (a n)n+(a rem n) | [div_rem_sum] |
| 9 |
Thm* a,b:, n:. ((a+bn) rem n) = (a rem n) | [rem_invariant] |
| 0 |
Thm* a:, n:. 0(a rem n) & (a rem n) < n | [rem_bounds_1] |
| 3 |
Thm* a:, n:. 0(a n) | [div_bounds_1] |
| 0 |
Thm* i1,i2,j1,j2:. i1j1 i2j2 i1+i2j1+j2 | [add_functionality_wrt_le] |