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

At: pos mul arg bounds 2 2

1. a:
2. b:
3. a < 0
4. b < 0

ab > 0

By: ReplaceWithEqv (TryC (HigherC IntSimpC)) ((-a)(-b) > 0) 0

Generated subgoal:

1 (-a)(-b) > 0


About:
intnatural_numberminusmultiplyless_than

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