a:
, n:
. a = (a 
n)
n+(a mod n)a:{...0}, n:. (a rem n) = -((-a) rem n)a:{...0}, b:. (a b) = -((-a) b)i,j:. i = j 
-i = -ja:, n:
. a = (a n)n+(a rem n)| Rank | Theorem | Name |
| 6 |
Thm* a:, n:. a = (a n)n+(a mod n) | [div_floor_mod_sum] |
| cites | ||
| 5 |
Thm* a:{...0}, n:. (a rem n) = -((-a) rem n) | [rem_2_to_1] |
| 4 |
Thm* a:{...0}, b:. (a b) = -((-a) b) | [div_2_to_1] |
| 0 | Thm* i,j:. i = j -i = -j | [minus_mono_wrt_eq] |
| 0 |
Thm* a:, n:. a = (a n)n+(a rem n) | [div_rem_sum] |