(2steps total) PrintForm Definitions int 2 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: div fun sat div nrel
  a:, n:. Div(a;n;a  n)
By: Def of Div(<nat>;<nat>;<nat>)

Generated subgoal:

1   a:, n:. n(a  n)  a < n((a  n)+1)
1 step

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

(2steps total) PrintForm Definitions int 2 Sections StandardLIB Doc