(6steps total) PrintForm Definitions Lemmas SimpleMulFacts Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: decidable prime 2 1 1
1. x:. Dec(prime(x))
2. x : 
3. x<0
  Dec(prime(x))
By: Rewrite by Thm*  y:. prime(-y)  prime(y)

Generated subgoals:

None

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

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