all
  (n:hnum. implies
  (n:hnum. (lt(0,n)
  (n:hnum. ,all
  (n:hnum. ,(q:hnum. all(r:hnum. equal(mod(add(mult(q,n),r),n),mod(r,n))))))

None

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