(22steps total)
PrintForm
Definitions
Lemmas
SimpleMulFacts
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
prime
nat
3
1
2
1
1
1.
x
:
2. 2
x
3.
(
i
:{2..
x
}.
i
|
x
)
4.
b
:
5. |
b
| |
x
6. |
b
| ~
b
|
b
| = 1
|
b
| =
x
By:
FwdThru:
Thm*
a
:
,
b
:
.
a
|
b
a
b
on [ Hyp:5 ]
Generated subgoal:
1
7. |
b
|
x
|
b
| = 1
|
b
| =
x
7
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(22steps total)
PrintForm
Definitions
Lemmas
SimpleMulFacts
Sections
DiscrMathExt
Doc