(5steps total) PrintForm Definitions Lemmas SimpleMulFacts Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nonprime nat
  x:. prime(x)  x<2  (i,j:{2..x}. x = ij)
By: UnivCD

Generated subgoal:

1 1. x : 
  prime(x)  x<2  (i,j:{2..x}. x = ij)
4 steps

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

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