is mentioned by

Thm* i:, j:{i...}. WellFnd{u}({i..j};x,y.x > y)	[int_seg_well_founded_down]
Thm* n:. WellFnd{i}({...n};x,y.x > y)	[int_lower_well_founded]
Thm* a:{...0}, n:{...-1}. 0(a rem n) & (a rem n) > n	[rem_bounds_3]
Thm* a:{...0}, n:. 0(a rem n) & (a rem n) > -n	[rem_bounds_2]
Thm* i:, n:. |i| > n i < -n i > n	[absval_lbound]
Thm* a,b:. ab < 0 a < 0 & b > 0 a > 0 & b < 0	[neg_mul_arg_bounds]
Thm* a,b:. ab > 0 a > 0 & b > 0 a < 0 & b < 0	[pos_mul_arg_bounds]
Thm* i,j:. i > j -i < -j	[minus_mono_wrt_lt]

Try larger context: StandardLIB