(4steps) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc

At: neg mul arg bounds 1

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:

13. -ab > -0 -a > -0 & b > 0 -a < -0 & b < 0
ab < 0 a < 0 & b > 0 a > 0 & b < 0


About:
intnatural_numberminusmultiplyless_thanandor

(4steps) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc