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

At: pos mul arg bounds 1

1. a:
2. b:
3. ab > 0

a > 0 & b > 0 a < 0 & b < 0

By:
Inst Thm* i,j:. i < j i = j i > j [a;0]
THEN
GenExRepD


Generated subgoals:

14. a < 0
a > 0 & b > 0 a < 0 & b < 0
24. a = 0
a > 0 & b > 0 a < 0 & b < 0
34. a > 0
a > 0 & b > 0 a < 0 & b < 0


About:
intnatural_numbermultiplyless_thanandor

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