is mentioned by

Thm*  p:. prime(p)  (b,z:. p | zb  b  0 & p | z)	[prime_divs_exp]
Thm*  X:.  Thm*  prime(X) Thm*   Thm*  (X1:. X1<X  prime(X1)  (a,b:. X1 | ab  X1 | a  X1 | b)) Thm*   Thm*  (W:. 0<W  W<X  (t:. X | tW  X | t))	[nat_prime_div_each_factorLEMMA]
Thm*  a,b:, P:({a..b}Prop), n:{(a+1)..(b+1)}. Thm*  P(n-1)  (i:{a..b}. ni  P(i))  (i:{a..b}. n-1i  P(i))	[extend_intseg_upperpart_down]

In prior sections: core well fnd int 1 bool 1 rel 1 LogicSupplement int 2 num thy 1 IteratedBinops

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