(10steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
At:
div
2
to
1
1
1
1
1
1
1
1
1.
a:
{...0}
2.
b:
3.
-b+b
(a
b) < -b
((-a)
b)
4.
-b+-b
((-a)
b) < b
(a
b)
(a
b) = -((-a)
b)
By:
AssertL [b
((a
b)-1) < b
(-((-a)
b));b
(-1+-((-a)
b)) < b
(a
b)]
Generated subgoal:
1
5.
b
((a
b)-1) < b
(-((-a)
b))
6.
b
(-1+-((-a)
b)) < b
(a
b)
(a
b) = -((-a)
b)
About:
(10steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc