is mentioned by

Thm* a:, n:, k:. k(a n) kna	[div_lbound_1]
Thm* a,b:. (a -- b) = 0 ab	[ndiff_zero]
Thm* a,b,c:. aimin(b;c) ab & ac	[imin_ub]
Thm* a,b,c:. imin(a;b)c ac bc	[imin_lb]
Thm* a,b,c:. aimax(b;c) ab ac	[imax_ub]
Thm* a,b,c:. imax(a;b)c ac & bc	[imax_lb]
Thm* P:(Prop). (x:. P(|x|)) (x:. P(x))	[absval_elim]
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* 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]
Thm* a,b,n:. ab a+nb+n	[add_mono_wrt_le_rw]
Thm* a,b,n:. ab a+nb+n	[add_mono_wrt_le]
Thm* a,b,n:. a < b a+n < b+n	[add_mono_wrt_lt_rw]
Thm* a,b,n:. a < b a+n < b+n	[add_mono_wrt_lt]
Thm* a,b,n:. a = b a+n = b+n	[add_mono_wrt_eq_rw]
Thm* a,b,n:. a = b a+n = b+n	[add_mono_wrt_eq]
Thm* i,j:. ij i < j+1	[le_to_lt_rw]
Thm* i,j:. i < j i+1j	[lt_to_le_rw]

In prior sections: core well fnd int 1 bool 1

Try larger context: StandardLIB