(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 1

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:
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