Nuprl Basics - Proof: sfa doc nat sqrt 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc nat sqrt 2

1. x :

2. 0<x
3.

. y

x-1 & x-1<(y+1)

(y+1)

. y

x & x<(y+1)

(y+1)

By:	ExistHD Hyp:-1

Generated subgoal:

1 3. y :
4. yyx-1
5. x-1<(y+1)(y+1)
y:. yyx & x<(y+1)(y+1)
3 steps

About:

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