Def  mod k == x,y://(m:. x-y = mk)

is mentioned by

Thm* 2 = 4   mod 2	[sfa_doc_zmod2_example]
Thm* f:(( mod 2)A). f  A	[sfa_doc_polymorph_example1]
Thm* k:.   ( mod k)	[sfa_doc_int_sub_int_mod]

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