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 |
| 3 | a,b:. ab>0 a>0 & b>0 a<0 & b<0 | [pos_mul_arg_bounds] |
| cites the following: | ||
| 0 | i,j:. i<j i = j i>j | [int_trichot] |
| 1 | a,b:, n:. na<nb a<b | [mul_cancel_in_lt] |
| 2 | a,b:. 0<ab | [mul_bounds_1b] |