Def  == {i:| i  0 }

is mentioned by

Thm* a:, b:. ab | a  (b ~ 1)	[self_divisor_mul]
Thm* a,b:, n:. ((na) ~ (nb))  (a ~ b)	[mul_cancel_in_assoced]
Thm* a:, n:. n | a  (a  n)n = a	[divides_iff_div_exact]
Thm* a:, b:. b | a  (a rem b) = 0	[divides_iff_rem_zero]
Def reducible(a) == b,c:. (b ~ 1) & (c ~ 1) & a = bc	[reducible]

In prior sections: int 1 int 2

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