is mentioned by

Thm* a:, n:. 0(a mod n) & (a mod n) < n	[mod_bounds]
Thm* a:, n:. q:. Div(a;n;q) & (a n) = q	[div_elim]
Thm* a:, n:{...-1}. 0(a rem n) & (a rem n) < -n	[rem_bounds_4]
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* a:, n:. 0(a rem n) & (a rem n) < n	[rem_bounds_1]
Thm* a,b,c:. aimin(b;c) ab & ac	[imin_ub]
Thm* a,b,c:. imax(a;b)c ac & bc	[imax_lb]
Thm* i:, n:. |i|n -ni & in	[absval_ubound]
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* a,b:. ab = 0 a = 0 & b = 0	[zero_ann_b]
Def Rem(a;n;r) == q:. Div(a;n;q) & qn+r = a	[rem_nrel]

In prior sections: core int 1 bool 1

Try larger context: StandardLIB