a:
, n:
. |a| < |n| 
(a rem n) = aa:
, n:
. a < n (a rem n) = ai:. |i| = ia:, n:. (a rem n) = -((-a) rem n)a:. -(-a) = aa:, n:. (a rem n) = (a rem -n)i:. |i| = |-i|| Rank | Theorem | Name |
| 8 |
Thm* a:, n:. |a| < |n| (a rem n) = a | [rem_gen_base_case] |
| cites | ||
| 7 |
Thm* a:, n:. a < n (a rem n) = a | [rem_base_case] |
| 0 |
Thm* i:. |i| = i | [absval_pos] |
| 7 |
Thm* a:, n:. (a rem n) = -((-a) rem n) | [rem_sym_1a] |
| 0 | Thm* a:. -(-a) = a | [minus_minus_cancel] |
| 6 |
Thm* a:, n:. (a rem n) = (a rem -n) | [rem_sym_2] |
| 1 |
Thm* i:. |i| = |-i| | [absval_sym] |