Def a mod n == if 0a a rem n ; ((-a) rem n)=0 0 else n-((-a) rem n) fi

is mentioned by

Thm* a:, n:. a = (a  n)n+(a mod n)	[div_floor_mod_sum]
Thm* a:, n:. 0(a mod n) & (a mod n)<n	[mod_bounds]

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