(15steps total)
Remark
PfGloss
PrintForm
Definitions
Lemmas
PrimesSquareRoots
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
primes
sqr
roots
LEMMA1
1
2
1.
a
:
2. prime(
a
)
3.
p
:
4.
q
:
5.
p
p
=
a
q
q
6.
a
|
p
p'
:
.
p'
<
p
&
q
q
=
a
p'
p'
By:
New:
p'
Analyze6
Generated subgoal:
1
6.
p'
:
7.
p
=
a
p'
p'
:
.
p'
<
p
&
q
q
=
a
p'
p'
11
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(15steps total)
Remark
PfGloss
PrintForm
Definitions
Lemmas
PrimesSquareRoots
Sections
DiscrMathExt
Doc