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  n) = ((a-n)  n)+1

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

1

8. (a  n)-1 = ((a-n)  n) & (a rem n) = ((a-n) rem n)   (a  n) = ((a-n)  n)+1

Auto

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