(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: rem rec case

  a:n:an  (a rem n) = ((a-n) rem n)

By: Auto THEN ElaborateDivision Auto 0


Generated subgoal:

1 1. a : 
2. n : 
3. an
4. a = (a  n)n+(a rem n)
5. a-n = ((a-n n)n+((a-n) rem n)
6. (a rem n n
7. ((a-n) rem n n
  (a rem n) = ((a-n) rem n)

1 step

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

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