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

At: neg mul arg bounds 1 1

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

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

By: RWH (RevLemmaC Thm* i,j:. i > j -i < -j) 3

Generated subgoal:

13. 0 > ab 0 > a & b > 0 a > 0 & b < 0
ab < 0 a < 0 & b > 0 a > 0 & b < 0


About:
intnatural_numberminusmultiplyless_thanandor

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