1. i : 
2. j : 
3. n : 
4. (i rem n)+(j rem n)
4. =
4. (((i rem n)+(j rem n))  n)n+(((i rem n)+(j rem n)) rem n)
5. i = (i  n)n+(i rem n)
6. j = (j  n)n+(j rem n)
7. i+j = ((i+j)  n)n+((i+j) rem n)
8. (i rem n)  n
9. (j rem n)  n
10. (((i rem n)+(j rem n)) rem n)  n
11. ((i+j) rem n)  n
  (((i rem n)+(j rem n)) rem n) = ((i+j) rem n)

By:	FwdThru:  Thm* k:, r1,r2:k, q1,q2:. q1k+r1 = q2k+r2  q1 = q2 & r1 = r2 on [ ((i  n)+(j  n)+(((i rem n)+(j rem n))  n))n on [ +(((i rem n)+(j rem n)) rem n) on [ = on [ ((i+j)  n)n+((i+j) rem n) ] {Auto would finish this now, but there would be too many steps for easy {reading. }

1

((i  n)+(j  n)+(((i rem n)+(j rem n))  n))n+(((i rem n)+(j rem n)) rem n)   =   ((i+j)  n)n+((i+j) rem n)

1 step

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