(11steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
At:
div
4
to
1
1
1
1
1
1
1
1
1
1
1
1.
a:
2.
b:
{...-1}
3.
(a
(-b)) < 1+-(a
b)
4.
-(a
b) < 1+(a
(-b))
5.
-(1+-(a
b)) < -(a
(-b))
6.
-(1+(a
(-b))) < -(-(a
b))
(a
b) = -(a
(-b))
By:
Auto
Generated subgoals:
None
About:
(11steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
(-b)) < 1+-(a b) b) < 1+(a (-b)) b)) < -(a (-b)) (-b))) < -(-(a b))
(a b) = -(a (-b))
