(10steps 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 gen base case 1 2 1

1. a : 
2. n : 
3. -a<n
4. 0a
5. ((-a) rem n) = -a
  (a rem n) = a


By: Rewrite-1 by Thm* a:b:. ((-a) rem b) = -(a rem b)


Generated subgoals:

None

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

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