PrintForm Definitions mb nat Sections MarkB generic Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: non neg sum

  n:f:(n). (x:n. 0f(x))  0sum(f(x) | x < n)

By: SumInd


Generated subgoals:

None

About:
intnatural_numberfunctionimpliesall
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

PrintForm Definitions mb nat Sections MarkB generic Search Doc