IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa doc nat sqrt211 1. x :
2. 0<x 3. y :
4. yyx-1
5. x-1<(y+1)(y+1)
6. x<(y+1)(y+1)
y:. yyx & x<(y+1)(y+1)
By:
Witness: y
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html