a,b:
. a
b < 0 
a < 0 & b > 0 
a > 0 & b < 0a,b:. ab > 0 a > 0 & b > 0 a < 0 & b < 0i,j:. i > j -i < -j| Rank | Theorem | Name |
| 5 |
Thm* a,b:. ab < 0 a < 0 & b > 0 a > 0 & b < 0 | [neg_mul_arg_bounds] |
| cites | ||
| 4 |
Thm* a,b:. ab > 0 a > 0 & b > 0 a < 0 & b < 0 | [pos_mul_arg_bounds] |
| 0 |
Thm* i,j:. i > j -i < -j | [minus_mono_wrt_lt] |