(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 1 2 1

1. a : 
2. prime(a)
3. p : 
4. q : 
5. pp = aqq
6. p' : 
7. p = ap'
8. a>0
9. p>0
10. p'>0
  aqq = aap'p'


By: Rewrite by aap'p' = ap'ap' { hyps Hyp:5 Hyp:7 } 


Generated subgoals:

None

About:
intnatural_numbermultiplyequal
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