a:
, n:
. (a mod n) 
a,b,n:. a+n
b+n 
abi,j:. i < j ija:, n:. 0(a rem n) & (a rem n) < n| Rank | Theorem | Name |
| 2 |
Thm* a:, n:. (a mod n) | [modulus_wf] |
| cites | ||
| 1 |
Thm* a,b,n:. a+nb+n ab | [add_cancel_in_le] |
| 0 | Thm* i,j:. i < j ij | [le_to_lt_weaken] |
| 0 |
Thm* a:, n:. 0(a rem n) & (a rem n) < n | [rem_bounds_1] |