(4steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
At:
neg
mul
arg
bounds
1
1
1.
a:
2.
b:
3.
-a
b > -0
-a > -0 & b > 0
-a < -0 & b < 0
a
b < 0
a < 0 & b > 0
a > 0 & b < 0
By:
RWH (RevLemmaC
Thm*
i,j:
. i > j
-i < -j) 3
Generated subgoal:
1
3.
0 > a
b
0 > a & b > 0
a > 0 & b < 0
a
b < 0
a < 0 & b > 0
a > 0 & b < 0
About:
(4steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc