is mentioned by

Thm* WellFnd{i}(;x,y.|x| < |y|)	[int_mag_well_founded]
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 rem n| < |n|	[rem_mag_bound]
Thm* a:, b:. |a rem b| < |b|	[rem_bounds_z]
Thm* P:(Prop). (x:. P(|x|)) (x:. P(x))	[absval_elim]
Thm* i:. |i| = |-i|	[absval_sym]
Thm* x,y:. |x| = |y| x = y	[absval_eq]
Thm* i:, n:. |i| > n i < -n i > n	[absval_lbound]
Thm* i:, n:. |i|n -ni & in	[absval_ubound]
Thm* i:. |i| = 0 i = 0	[absval_zero]
Thm* i:{...0}. |i| = -i	[absval_neg]
Thm* i:. |i| = i	[absval_pos]

Try larger context: StandardLIB