is mentioned by

Thm* a:, b:. |a| = |b| (a rem b) = 0	[rem_eq_args_z]
Thm* a:, b:. |a| < |b| (a rem b) = a	[rem_base_case_z]
Thm* a:, n:. |a| < |n| (a rem n) = a	[rem_gen_base_case]
Thm* a:, n:. (a n)	[divide_wfa]
Thm* a:, n:. |a rem n| < |n|	[rem_mag_bound]
Thm* a:, n:. (a rem n) = (a rem -n)	[rem_sym_2]
Thm* a:, n:. (a rem n) = -((-a) rem n)	[rem_sym_1a]
Thm* a:, n:. -(a rem n) = ((-a) rem n)	[rem_sym_1]
Thm* a:, b:. |a rem b| < |b|	[rem_bounds_z]
Thm* a:, b:. ((-a) rem b) = -(a rem b)	[rem_antisym]
Thm* a:, b:. (a rem -b) = (a rem b)	[rem_sym]
Thm* a:, n:. (a rem n) = a-(a n)n	[rem_to_div]
Thm* a:, n:. a = (a n)n+(a rem n)	[div_rem_sum]
Thm* a,b:, n:. na = nb a = b	[mul_cancel_in_eq]

In prior sections: int 1

Try larger context: StandardLIB