Gloss of Lemma enabling rewrite of (pp = aqq) to (qq = ap'p').

Thm*  a:. 
Thm*  prime(a)  (p:, q:. pp = aqq  (p':. p'<p & qq = ap'p'))

Since a divides pp, and is prime, it also divides p, by

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

so let p = ap'.

Note that a, p, and p' must be positive,
since prime(a), aqq>0, pp>0, and ap'>0.

So these are equal:

aqq, pp, ap'ap', aap'p'

and qq = ap'p' by cancellation of a.

And p'<p, since p = ap' and 1<a, since prime(a).

QED

About: IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html