(8steps total) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: rem sym 1 1
1. a : 
2. b : 
3. a = (a  (-b))(-b)+(a rem -b)
4. a = (a  b)b+(a rem b)
  (a rem -b) = (a rem b)
By: Decide: 0a THEN BoundRem Auto 0

Generated subgoals:

1 5. 0a
6. (a rem -b)  (-(-b))
7. (a rem b)  b
  (a rem -b) = (a rem b)
1 step
2 5. 0a
6. -(a rem -b)  (-(-b))
7. -(a rem b)  b
  (a rem -b) = (a rem b)
1 step

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

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