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

At: pos mul arg bounds 2

1. a:
2. b:
3. a > 0 & b > 0 a < 0 & b < 0

ab > 0

By: GenExRepD

Generated subgoals:

13. a > 0
4. b > 0
ab > 0
23. a < 0
4. b < 0
ab > 0


About:
intnatural_numbermultiplyless_thanandor

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