Def i =  j == i = j    i = -j

is mentioned by

Thm* a,b:. a | b & b | a  a =  b	[assoc_reln]
Thm* a,b:. a | b  b | a  a =  b	[divides_anti_sym]
Thm* b:. b | 1  b =  1	[only_pm_one_divs_one]

In prior sections: int 2

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