a:
, b:
. |a rem b| < |b|a:, b:. ((-a) rem b) = -(a rem b)a:
, n:
. 0
(a rem n) & (a rem n) < ni:. |i| = ii:. |i| = |-i|a:, b:. (a rem -b) = (a rem b)| Rank | Theorem | Name |
| 8 |
Thm* a:, b:. |a rem b| < |b| | [rem_bounds_z] |
| cites | ||
| 7 |
Thm* a:, b:. ((-a) rem b) = -(a rem b) | [rem_antisym] |
| 0 |
Thm* a:, n:. 0(a rem n) & (a rem n) < n | [rem_bounds_1] |
| 0 |
Thm* i:. |i| = i | [absval_pos] |
| 1 |
Thm* i:. |i| = |-i| | [absval_sym] |
| 6 |
Thm* a:, b:. (a rem -b) = (a rem b) | [rem_sym] |