Def ij == ji

is mentioned by

Thm* a:, n:. an  (a rem n) = ((a-n) rem n)	[rem_rec_case]
Thm* a:, n:. an  (a  n) = ((a-n)  n)+1	[div_rec_case]
Thm* a:{...0}, n:{...-1}. 0(a rem n) & (a rem n)>n	[rem_bounds_3]
Thm* a:{...0}, n:. 0(a rem n) & (a rem n)>-n	[rem_bounds_2]

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