Nuprl - FTA LEMMAs for nat_prime_div_each

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Rank	Theorem	Name
16	Thm* X:. prime(X) (a,b:. X \| ab X \| a X \| b)	[nat_prime_div_each_factor]
cites the following:
15	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]
0	Thm* a:, b:. q:, r:b. a = qb+r	[quot_rem_exists_n]
11	Thm* x:. prime(x) 2x	[natprimes_lb]
3	Thm* k:, n:, x,y:. kx+n = ky xy	[factor_bound]
2	Thm* a,b:. a \| b (c:. b = ac)	[divides_def_on_nat]
1	Thm* a:, b:. a \| b ab	[divisor_bound]

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html