(12steps total)
PrintForm
Definitions
Lemmas
num
thy
1
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
coprime
iff
ndivides
2
1
1
1.
a
:
2.
p
:
3. prime(
p
)
4.
p
|
a
5.
c
:
6.
c
|
p
7.
c
|
a
8.
p
= 0
9.
(
p
~ 1)
10.
a
:
.
a
|
p
(
a
~ 1)
(
a
~
p
)
c
| 1
By:
FwdThru 10 [6]
Generated subgoal:
1
11. (
c
~ 1)
(
c
~
p
)
c
| 1
3
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(12steps total)
PrintForm
Definitions
Lemmas
num
thy
1
Sections
StandardLIB
Doc