is mentioned by

Thm* a,b,c:. imin(a;b)c ac bc	[imin_lb]
Thm* a,b,c:. aimax(b;c) ab ac	[imax_ub]
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* a,b:. ab = 0 a = 0 b = 0	[int_entire]
Thm* a,b:. a = 0 b = 0 ab = 0	[zero_ann_a]
Def i = j == i = j i = -j	[pm_equal]

In prior sections: core bool 1

Try larger context: StandardLIB