(4steps)
PrintForm
Definitions
int
2
Sections
StandardLIB
Doc
At:
absval
lbound
1
1.
i:
2.
n:
|i| > n
i < -n
i > n
By:
Unfold `absval` 0
THEN
SplitOnConclITE
Generated subgoals:
1
3.
0
i
i > n
i < -n
i > n
2
3.
i < 0
-i > n
i < -n
i > n
About:
(4steps)
PrintForm
Definitions
int
2
Sections
StandardLIB
Doc
i
i > n 
i < -n 
i > n -i > n i < -n i > n
|i| > n i < -n i > ni i > n i < -n i > n -i > n i < -n i > n
