(3steps 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 base case 1

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


By: FwdThru: 
Thm* k:r1,r2:kq1,q2:q1k+r1 = q2k+r2  q1 = q2 & r1 = r2
on [ (a  n)n+(a rem n) = 0n+a ]


Generated subgoal:

1 6. (a  n) = 0 & (a rem n) = a
  (a rem n) = a

Auto

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

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