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

Thm*  p:, q:. pp = 2qq  (p':. p'<p & qq = 2p'p')

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

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

so let p = 2p'.

Note that 2, p, and p' must be positive,
since 2qq>0, pp>0, and 2p'>0.

So these are equal:

2qq, pp, 2p'2p', 22p'p'

and qq = 2p'p' by cancellation of 2.

And p'<p, since p = 2p'.

QED

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