(9steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
nsub
mul
2
2
1
1
1.
a
:
2. 0<
a
3.
b
,
c
:
. (
a
-1)
b
=
c
((
(
a
-1)
b
) ~
c
)
4.
b
:
5.
c
:
6.
a
b
=
c
7. 1
b
a
b
(
(
c
-
b
)+
b
) ~
c
By:
BackThru:
Thm*
c
,
a
,
b
:
.
a
+
b
=
c
((
a
+
b
) ~
c
)
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(9steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
b,c:
. (a-1)
b = c 
((
a
(
