a,b:
, n:
. ((a+b
n) rem n) = (a rem n)i,j:
. i < j 
i+1
ja,b:, n:. ab 
nanbi1,i2,j1,j2:. i1j1 i2j2 i1+i2j1+j2a:, n:. a
n (a rem n) = ((a-n) rem n)| Rank | Theorem | Name |
| 9 |
Thm* a,b:, n:. ((a+bn) rem n) = (a rem n) | [rem_invariant] |
| cites | ||
| 1 |
Thm* i,j:. i < j i+1j | [lt_to_le_rw] |
| 1 |
Thm* a,b:, n:. ab nanb | [mul_preserves_le] |
| 0 |
Thm* i1,i2,j1,j2:. i1j1 i2j2 i1+i2j1+j2 | [add_functionality_wrt_le] |
| 8 |
Thm* a:, n:. an (a rem n) = ((a-n) rem n) | [rem_rec_case] |