(4steps total)
PrintForm
Definitions
Lemmas
SimpleMulFacts
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
only
one
nat
divs
one
1
1.
b
:
2.
b
| 1
b
= 1
By:
FwdThru:
Thm*
a
,
b
:
.
a
|
b
(
c
:
.
b
=
a
c
) on [
b
| 1 ]
Generated subgoal:
1
3.
c
:
. 1 =
b
c
b
= 1
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(4steps total)
PrintForm
Definitions
Lemmas
SimpleMulFacts
Sections
DiscrMathExt
Doc
b = 1
b = 1
a,b:. a | b 
(
c:. b = a
c) on [ b | 1 ]c:. 1 = bc
b = 1
