(5steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
No number smaller than the least one having a property has it.

At: least is least2

  p:{p:()| i:. p(i) }, j:(least i:. p(i)). p(j)
By: Analyze

Generated subgoal:

1 1. p : {p:()| i:. p(i) }
  j:(least i:. p(i)). p(j)
4 steps

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

(5steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc