(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 1 1
1. x : 
  2x  (i:{2..x}. i | x)  x<2  (i,j:{2..x}. x = ij)
By: Auto THEN SimilarTo: Hyp:-1

Generated subgoal:

1 2. i : {2..x}
3. c : 
4. x = ic
  c  {2..x}
2 steps

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

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