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