x:
, n:
. ((-x) mod n) = if (x mod n)=
0
0 else n-(x mod n) fia:, n:. a = (a 
n)
n+(a mod n) & (a mod n) < na:, n:, q:, r:. a = qn+r 
r < n q = (a n) & r = (a mod n)| Rank | Theorem | Name |
| 7 | Thm* x:, n:. ((-x) mod n) = if (x mod n)=0 0 else n-(x mod n) fi | [mod_minus] |
| cites | ||
| 2 | Thm* a:, n:. a = (a n)n+(a mod n) & (a mod n) < n | [div_floor_mod_properties] |
| 6 | Thm* a:, n:, q:, r:. a = qn+r r < n q = (a n) & r = (a mod n) | [div_floor_mod_unique] |