(10steps 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: two sqr roots LEMMA1 1 2 1 1 1
1. prime(2)
2. p : 
3. q : 
4. pp = 2qq
5. p' : 
6. p = 2p'
7. 2>0
8. p>0
9. p'>0
  qq = 2p'p'
By: Use:[n:= 2] BackThru: Thm: mul cancel in eq

Generated subgoal:

1   2qq = 22p'p'
1 step

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

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