(11steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
At:
div
4
to
1
1
1
1.
a:
2.
b:
{...-1}
3.
a = (a
(-b))
(-b)+(a rem -b)
4.
0
(a rem -b) & (a rem -b) < -b
5.
a = (a
b)
b+(a rem b)
6.
0
(a rem b) & (a rem b) < -b
(a
b) = -(a
(-b))
By:
Analyze 6
THEN
Analyze 4
Generated subgoal:
1
4.
0
(a rem -b)
5.
(a rem -b) < -b
6.
a = (a
b)
b+(a rem b)
7.
0
(a rem b)
8.
(a rem b) < -b
(a
b) = -(a
(-b))
About:
(11steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc