a:
, b:
. ((-a) rem b) = -(a rem b)a:{...0}, n:
. (a rem n) = -((-a) rem n)a:, b:. (a rem -b) = (a rem b)| Rank | Theorem | Name |
| 7 |
Thm* a:, b:. ((-a) rem b) = -(a rem b) | [rem_antisym] |
| cites | ||
| 5 |
Thm* a:{...0}, n:. (a rem n) = -((-a) rem n) | [rem_2_to_1] |
| 6 |
Thm* a:, b:. (a rem -b) = (a rem b) | [rem_sym] |