is mentioned by

Thm* a:, n:. 0(a mod n) & (a mod n) < n	[mod_bounds]
Thm* a:, n:, k:. k(a n) kna	[div_lbound_1]
Thm* a:, n:. 0(a n)	[div_bounds_1]
Thm* a:, n:{...-1}. 0(a rem n) & (a rem n) < -n	[rem_bounds_4]
Thm* a:, n:. 0(a rem n) & (a rem n) < n	[rem_bounds_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* i:, n:. |i|n -ni & in	[absval_ubound]
Thm* a,b:. 0ab	[mul_bounds_1a]
Thm* i1,i2,j1,j2:. i1j1 i2j2 i1i2j1j2	[multiply_functionality_wrt_le]
Thm* a,b:, n:. nanb ab	[mul_cancel_in_le]
Thm* a,b:, n:. ab nanb	[mul_preserves_le]
Thm* i1,i2,j1,j2:. i1j1 i2j2 i1-i2j1-j2	[sub_functionality_wrt_le]
Thm* i,j:. ij -i-j	[minus_functionality_wrt_le]
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+nb+n ab	[add_cancel_in_le]
Thm* i1,i2,j1,j2:. i1 < j1 i2j2 i1+i2 < j1+j2	[add_functionality_wrt_lt]
Thm* i1,i2,j1,j2:. i1j1 i2j2 i1+i2j1+j2	[add_functionality_wrt_le]
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: int 1 bool 1 core

Try larger context: StandardLIB