Nuprl - Proof: primes sqr roots LEMMA1 1 2 1 1 1

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

1. a :

2. prime(a)
3. p :

4. q :

5. p

p = a

q
6. p' :

7. p = a

p'
8. a>0
9. p>0
10. p'>0

p'<p

By:	Use:[n:= a] BackThru: Thm* a,b:, n:. na<nb a<b

Generated subgoal:

1 ap'<ap
4 steps

About:

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