Nuprl - Proof: two sqr roots 1 1 1 1 1

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

1. p :

2. q :

3. p

p = 2

q
4.

, q:

. p

p = 2

(

p':

. p'<p & q

q = 2

p')
5. p' :

6. p'<p
7. q

q = 2

p'
8. q' :

9. q'<q
10. p'

p' = 2

p':

. p'<p & (

q':

. p'

p' = 2

q')

By:	Witness: p' THEN Witness: q'

Generated subgoals:

None

About:

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