Lemma for Thm: two sqr roots, rewriting (pp = 2qq) to (qq = 2p'p')

At: two sqr roots LEMMA1

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

By:	Use:[2] (ApplyDecideLemma Thm*  x:. Dec(prime(x)))

1

1. prime(2) 2. p :  3. q :  4. pp = 2qq   p':. p'<p & qq = 2p'p'

9 steps

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