Def nondecreasing(f;k) == i:(k-1). f(i)f(i+1)

is mentioned by

Thm* n:, f,g:(n). Thm* increasing(f;n)  nondecreasing(g;n)  increasing(fadd(f;g);n)	[fadd_increasing]
Thm* k:, x:. nondecreasing(i.x;k)	[const_nondecreasing]

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