a:
, b:
. |a| = |b| 
(a rem b) = 0a:
. (a rem a) = 0a:, n:. -(a rem n) = ((-a) rem n)a:, b:. (a rem -b) = (a rem b)i:. |i| = |-i|| Rank | Theorem | Name |
| 6 | a:, b:. |a| = |b| (a rem b) = 0 | [rem_eq_args_z] |
| cites the following: | ||
| 3 | a:. (a rem a) = 0 | [rem_eq_args] |
| 5 | a:, n:. -(a rem n) = ((-a) rem n) | [rem_sym_1] |
| 3 | a:, b:. (a rem -b) = (a rem b) | [rem_sym] |
| 0 | i:. |i| = |-i| | [absval_sym] |