At: neg mul arg bounds1 1. a: 2. b: 3. (-a)b > 0 -a > 0 & b > 0 -a < 0 & b < 0
ab < 0 a < 0 & b > 0 a > 0 & b < 0 By: ReplaceWithEqv (TryC (HigherC IntSimpC)) (-ab > -0 -a > -0 & b > 0 -a < -0 & b < 0) 3 Generated subgoal: