a:
, n:
. 0
(a mod n) & (a mod n) < na:, n:. (a mod n) 
a,b,n:. a+n < b+n 
a < ba:, n:. 0(a rem n) & (a rem n) < n| Rank | Theorem | Name |
| 3 |
Thm* a:, n:. 0(a mod n) & (a mod n) < n | [mod_bounds] |
| cites | ||
| 2 |
Thm* a:, n:. (a mod n) | [modulus_wf] |
| 2 |
Thm* a,b,n:. a+n < b+n a < b | [add_cancel_in_lt] |
| 0 |
Thm* a:, n:. 0(a rem n) & (a rem n) < n | [rem_bounds_1] |