all
  (n:hnum. implies
  (n:hnum. (lt(0,n)
  (n:hnum. ,all
  (n:hnum. ,(j:hnum. all
  (n:hnum. ,(j:hnum. (k:hnum. equal
  (n:hnum. ,(j:hnum. (k:hnum. (mod(add(mod(j,n),mod(k,n)),n)
  (n:hnum. ,(j:hnum. (k:hnum. ,mod(add(j,k),n))))))

None

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