Def  prime(a) == a = 0 & (a ~ 1) & (b,c:. a | bc  a | b  a | c)

is mentioned by

Thm*  a:. prime(a)  (p:, q:. pp = aqq)	[primes_sqr_roots]
Thm*  a:.  Thm*  prime(a)  (p:, q:. pp = aqq  (p':. p'<p & qq = ap'p'))	[primes_sqr_roots_LEMMA1]
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