At:
absval mul222
1.
a:
2.
b:
3.
a = 0
4.
b = 0
5.
0ab
6.
a < 0
7.
0b
ab = (-a)b
By:
AssertBY (ab < 0)
(BackThru
Thm*a,b:. ab < 0 a < 0 & b > 0 a > 0 & b < 0)
THEN
Try (OrLeft THEN (Complete Auto))
THEN
Try (OrRight THEN (Complete Auto))
Generated subgoals:
a = 0
a
b
a
a,b:
a < 0 & b > 0 
a > 0 & b < 0)