(2steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
There are as many positive numbers as non-negative.

At: nat plus ooc nat

   ~ 
By: Witness: x.x-1 | y.y+1

Generated subgoal:

1   InvFuns(;;x.x-1;y.y+1)
1 step

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

(2steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Search Doc