a:
, b:
. |a| = |b| 
(a rem b) = 0a:, b:. ((-a) rem b) = -(a rem b)i,j:. i = j 
-i = -ja:
. (a rem a) = 0a:, b:. (a rem -b) = (a rem b)| Rank | Theorem | Name |
| 10 |
Thm* a:, b:. |a| = |b| (a rem b) = 0 | [rem_eq_args_z] |
| cites | ||
| 7 |
Thm* a:, b:. ((-a) rem b) = -(a rem b) | [rem_antisym] |
| 0 | Thm* i,j:. i = j -i = -j | [minus_mono_wrt_eq] |
| 9 |
Thm* a:. (a rem a) = 0 | [rem_eq_args] |
| 6 |
Thm* a:, b:. (a rem -b) = (a rem b) | [rem_sym] |