is mentioned by

Thm* i:, j:{i...}. WellFnd{u}({i..j};x,y.x>y)	[int_seg_well_founded_down]
Thm* n:. WellFnd{i}({...n};x,y.x>y)	[int_lower_well_founded]
Thm* a:{...0}, n:{...-1}. 0(a rem n) & (a rem n)>n	[rem_bounds_3]
Thm* a:{...0}, n:. 0(a rem n) & (a rem n)>-n	[rem_bounds_2]
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]

Try larger context: StandardLIB IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html