(8steps total) Gloss PrintForm Definitions NumThyExamples Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: quot rem exists n sfa
  a:, b:. q:, r:b. a = qb+r
By: hold b constant

Generated subgoal:

1 1. b : 
  a:. q:, r:b. a = qb+r
7 steps

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

(8steps total) Gloss PrintForm Definitions NumThyExamples Sections NuprlLIB Doc