Def mod == m:. n:. nmod(m;n)

is mentioned by

Thm* all(k:hnum. equal(mod(k,suc(0)),0))	[hmod_one]
Thm* all Thm* (n:hnum. implies Thm* (n:hnum. (lt(0,n) Thm* (n:hnum. ,all Thm* (n:hnum. ,(k:hnum. and Thm* (n:hnum. ,(k:hnum. (equal(k,add(mult(div(k,n),n),mod(k,n))) Thm* (n:hnum. ,(k:hnum. ,lt(mod(k,n),n)))))	[hdivision]

Try larger context: HOLlib IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html