Def   == {i:| i  0 }

is mentioned by

Thm*  a,b:, m,n:. m = n  (ma = nb  a = b)	[mul_cancel_in_eq2]
Thm*  a,b:, n:. na = nb  a = b	[mul_cancel_in_eq1]

In prior sections: int 1 int 2 num thy 1

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