At:
absval mul224
1.
a:
2.
b:
3.
a = 0
4.
b = 0
5.
ab < 0
6.
a < 0
7.
b < 0
-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
b < 0
-a
a,b:
a > 0 & b > 0 
a < 0 & b < 0)