Nuprl - Proof: two sqr roots LEMMA1 1 2 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: two sqr roots LEMMA1 1 2 1

1. prime(2)
2. p :

3. q :

4. p

p = 2

q
5. p' :

6. p = 2

p':

. p'<p & q

q = 2

By:	2>0 & p>0 & p'>0 By SideProof

Generated subgoal:

1 7. 2>0
8. p>0
9. p'>0
p':. p'<p & qq = 2p'p'
3 steps

About:

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