(2steps total) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: division typing1a sfa

  a:n:. (a  n 

By: Auto THEN ElaborateDivision Auto 0


Generated subgoal:

1 1. a : 
2. n : 
3. a = (a  n)n+(a rem n)
4. (a rem n n
  0(a  n)

1 step

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

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