Nuprl - Proof: primes sqr roots LEMMA1 1

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

1. a :

2. prime(a)
3. p :

4. q :

5. p

p = a

p':

. p'<p & q

q = a

By:	FwdThru: Thm* a:. prime(a) (x:. a \| xx a \| x) on [ a \| pp ]

Generated subgoals:

1 a | pp
1 step

2 6. a | p
p':. p'<p & qq = ap'p'
12 steps

About:

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