(7steps total)
PrintForm
Definitions
Lemmas
FTA
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
prime
divs
exp
1
1
1
1.
p
:
2. prime(
p
)
3.
b
:
4.
z
:
5.
p
|
z
b
6.
b
= 0
False
By:
Rewrite5 by
b
= 0 ...
THEN Compute-1
z
0 *
1
Generated subgoal:
1
7.
p
| 1
False
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(7steps total)
PrintForm
Definitions
Lemmas
FTA
Sections
DiscrMathExt
Doc