a:{...0}, n:{...-1}. (a rem n) = -((-a) rem -n)a:
, n:
. (a rem n) = a-(a 
n)
na:{...0}, b:{...-1}. (a b) = ((-a) (-b))| Rank | Theorem | Name |
| 5 |
Thm* a:{...0}, n:{...-1}. (a rem n) = -((-a) rem -n) | [rem_3_to_1] |
| cites | ||
| 1 |
Thm* a:, n:. (a rem n) = a-(a n)n | [rem_to_div] |
| 4 |
Thm* a:{...0}, b:{...-1}. (a b) = ((-a) (-b)) | [div_3_to_1] |