(2steps total)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
div
2
to
1
a
:{...0},
b
:
. (
a
b
) = -((-
a
)
b
)
By:
Auto THEN ElaborateDivision Auto 0
Generated subgoal:
1
1.
a
: {...0}
2.
b
:
3.
a
= (
a
b
)
b
+(
a
rem
b
)
4. -
a
= ((-
a
)
b
)
b
+((-
a
) rem
b
)
5. -(
a
rem
b
)
b
6. ((-
a
) rem
b
)
b
(
a
b
) = -((-
a
)
b
)
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
a:{...0}, b:
. (a 
b) = -((-a) b) a:{...0}, b:. (a b) = -((-a) b)
b)
b+(a rem b)
b)b+((-a) rem b)
b
b
(a b) = -((-a) b)
