(6steps total) PrintForm Definitions NuprlPrimitives Sections NuprlLIB Doc
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:yyx-1 & x-1<(y+1)(y+1)
  y:yyx & 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:
intnatural_numberaddsubtractmultiplyless_thanandexists
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(6steps total) PrintForm Definitions NuprlPrimitives Sections NuprlLIB Doc