(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
4
to
1
a
:
,
b
:{...-1}. (
a
b
) = -(
a
(-
b
))
By:
Auto THEN ElaborateDivision Auto 0
Generated subgoal:
1
1.
a
:
2.
b
: {...-1}
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:
, b:{...-1}. (a 
b) = -(a (-b)) a:, b:{...-1}. (a b) = -(a (-b))
b)
b+(a rem b)
(-b))(-b)+(a rem -b)
(-b)
(-b)
(a b) = -(a (-b))
