PrintForm Definitions mb nat Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: fadd increasing

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


By: Unfolds [`increasing`;`nondecreasing`;`fadd`] 0 THEN Reduce 0
THEN
AllHyps (InstHyp [i])


Generated subgoals:

None

About:
intnatural_numberfunctionimpliesall
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

PrintForm Definitions mb nat Sections MarkB generic Doc