a:
, b:
. |a| < |b| 
(a rem b) = aa:
, n:{...-1}. (a rem n) = (a rem -n)a:{...0}, n:
. (a rem n) = -((-a) rem n)a:, n:. a < n (a rem n) = aa:{...0}, n:{...-1}. (a rem n) = -((-a) rem -n)| Rank | Theorem | Name |
| 8 |
Thm* a:, b:. |a| < |b| (a rem b) = a | [rem_base_case_z] |
| cites | ||
| 5 |
Thm* a:, n:{...-1}. (a rem n) = (a rem -n) | [rem_4_to_1] |
| 5 |
Thm* a:{...0}, n:. (a rem n) = -((-a) rem n) | [rem_2_to_1] |
| 7 |
Thm* a:, n:. a < n (a rem n) = a | [rem_base_case] |
| 5 |
Thm* a:{...0}, n:{...-1}. (a rem n) = -((-a) rem -n) | [rem_3_to_1] |