a:
, n:
. |a|<|n| 
(a rem n) = aa:
, n:
. a<n (a rem n) = aa:, b:. ((-a) rem b) = -(a rem b)a:, b:. (a rem -b) = (a rem b)i:. |i| = |-i|| Rank | Theorem | Name |
| 5 | a:, n:. |a|<|n| (a rem n) = a | [rem_gen_base_case] |
| cites the following: | ||
| 3 | a:, n:. a<n (a rem n) = a | [rem_base_case] |
| 4 | a:, b:. ((-a) rem b) = -(a rem b) | [rem_antisym] |
| 3 | a:, b:. (a rem -b) = (a rem b) | [rem_sym] |
| 0 | i:. |i| = |-i| | [absval_sym] |