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