Nuprl - PrimesSquareRoots LEMMAs for primes_sqr_roots

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

Rank	Theorem	Name
11	Thm* a:. Thm* prime(a) (p:, q:. pp = aqq (p':. p'<p & qq = ap'p'))	[primes_sqr_roots_LEMMA1]
cites the following:
1	Thm* a:. prime(a) (x:. a \| xx a \| x)	[prime_divides_square]
3	Thm* a,b:. ab>0 a>0 & b>0 a<0 & b<0	[pos_mul_arg_bounds]
1	Thm* a,b:, n:. na<nb a<b	[mul_cancel_in_lt]
0	Thm* a,b:. ab = ba	[mul_com]
1	Thm* a,b:, n:. a<b na<nb	[mul_preserves_lt]
10	Thm* x:. prime(x) 2x & (i:{2..x}. i \| x)	[prime_nat]
3	Thm* a,b:, n:. na = nb a = b	[mul_cancel_in_eq]

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