is mentioned by

Thm* i:, j:{i+1...}, E:({i..j}Prop). Thm* E(i)  (k:{(i+1)..j}. E(k-1)  E(k))  (k:{i..j}. E(k))	[int_seg_ind]
Thm* i:, E:({...i}Prop). Thm* E(i)  (k:{...i-1}. E(k+1)  E(k))  (k:{...i}. E(k))	[int_lower_ind]
Thm* i:, E:({i...}Prop). Thm* E(i)  (k:{i+1...}. E(k-1)  E(k))  (k:{i...}. E(k))	[int_upper_ind]
Thm* k:, r1,r2:k, q1,q2:. q1k-r1 = -(q2k+r2)  q1 = -q2 & r1 = r2	[division3_sfa]
Thm* k:, r1,r2:k, q1,q2:. q1k-r1 = q2k-r2  q1 = q2 & r1 = r2	[division2_sfa]
Thm* k:, r1,r2:k, q1,q2:. q1k+r1 = q2k+r2  q1 = q2 & r1 = r2	[division1_sfa]
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 IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html