all
  (n:hnum. implies
  (n:hnum. (lt(0,n)
  (n:hnum. ,all
  (n:hnum. ,(k:hnum. and
  (n:hnum. ,(k:hnum. (equal(k,add(mult(div(k,n),n),mod(k,n)))
  (n:hnum. ,(k:hnum. ,lt(mod(k,n),n)))))

1	1. n :  2. 0<n 3. k :    k = ndiv(k;n)n+nmod(k;n)	3 steps
2	1. n :  2. 0<n 3. k :    nmod(k;n)<n	2 steps

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