is mentioned by

Thm* i:, j:{i+1...}, E:({i..j}Prop). E(i) (k:{(i+1)..j}. E(k-1) E(k)) (k:{i..j}. E(k))	[int_seg_ind]
Thm* i:, E:({...i}Prop). E(i) (k:{...i-1}. E(k+1) E(k)) (k:{...i}. E(k))	[int_lower_ind]
Thm* i:, E:({i...}Prop). E(i) (k:{i+1...}. E(k-1) E(k)) (k:{i...}. E(k))	[int_upper_ind]
Thm* a,b,c:. aimin(b;c) ab & ac	[imin_ub]
Thm* a,b,c:. imax(a;b)c ac & bc	[imax_lb]
Thm* a,b,n:. ab a+nb+n	[add_mono_wrt_le_rw]
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_eq_rw]
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