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

At: pos mul arg bounds 1 3
1. a:
2. b:
3. ab > 0
4. a > 0

a > 0 & b > 0 a < 0 & b < 0
By: Sel 1 (Analyze 0)
Generated subgoal:

1 b > 0

About:
intnatural_numbermultiplyless_thanandor

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