(15steps total) Remark 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 LEMMA1 1 2

1. a : 
2. prime(a)
3. p : 
4. q : 
5. pp = aqq
6. a | p
  p':p'<p & qq = ap'p'


By: New:p' Analyze6


Generated subgoal:

1 6. p' : 
7. p = ap'
  p':p'<p & qq = ap'p'

11 steps

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

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