a,b:
. a
b > 0 
a > 0 & b > 0 
a < 0 & b < 0i,j:. i < j i = j i > ja,b:, n:
. na < nb 
a < ba,b:. 0 < ab| Rank | Theorem | Name |
| 4 |
Thm* a,b:. ab > 0 a > 0 & b > 0 a < 0 & b < 0 | [pos_mul_arg_bounds] |
| cites | ||
| 0 | Thm* i,j:. i < j i = j i > j | [int_trichot] |
| 2 |
Thm* a,b:, n:. na < nb a < b | [mul_cancel_in_lt] |
| 3 |
Thm* a,b:. 0 < ab | [mul_bounds_1b] |