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

At: neg mul arg bounds


a,b:. ab < 0 a < 0 & b > 0 a > 0 & b < 0

By:
RepD
THEN
Inst Thm* a,b:. ab > 0 a > 0 & b > 0 a < 0 & b < 0 [-a;b]


Generated subgoal:

11. 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


About:
intnatural_numberminusmultiplyless_thanandorall

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