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