(22steps total) PrintForm Definitions Lemmas SimpleMulFacts Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: prime nat 3
1. x : 
2. 2x
3. (i:{2..x}. i | x)
  prime(x)
By: BackThru: Thm*  a:. atomic(a)  prime(a)

Generated subgoal:

1   atomic(x)
15 steps

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

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