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

1. a : 
2. n : 
3. k : 
4. a = (a  n)n+(a rem n)
5. (a rem n n
  k(a  n kna


By: Auto


Generated subgoals:

1 6. k(a  n)
  kna

1 step
2 6. kna
  k(a  n)

1 step

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

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