(7steps total) PfGloss PrintForm Definitions Lemmas PrimesSquareRoots Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: primes sqr roots 1 1

1. a : 
2. prime(a)
3. p : 
4. q:pp = aqq
  p':p'<p & (q':p'p' = aq'q')


By: Analyze4


Generated subgoal:

1 4. q : 
5. pp = aqq
  p':p'<p & (q':p'p' = aq'q')

4 steps

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

(7steps total) PfGloss PrintForm Definitions Lemmas PrimesSquareRoots Sections DiscrMathExt Doc