Def  b | a == c:. a = bc

is mentioned by

Thm*  a:. prime(a)  (x:. a | xx  a | x)

[prime_divides_square]

In prior sections: num thy 1 SimpleMulFacts

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