is mentioned by

Thm* n:, f,g:(n). Thm* increasing(f;n)  nondecreasing(g;n)  increasing(fadd(f;g);n)

[fadd_increasing]

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