(15steps total) PfGloss PrintForm Definitions Lemmas PrimesSquareRoots Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Lemma for Thm: primes sqr roots, rewriting (pp = aqq) to (qq = ap'p')

At: primes sqr roots LEMMA1

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

Generated subgoal:

1 1. a : 
2. prime(a)
3. p : 
4. q : 
5. pp = aqq
  p':. p'<p & qq = ap'p'
14 steps

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

(15steps total) PfGloss PrintForm Definitions Lemmas PrimesSquareRoots Sections DiscrMathExt Doc