a,b:
. a | b 
(
c:. b = a
c 
)a,b:
. ab>0 a>0 & b>0 
a<0 & b<0a,b:. 0<ab| Rank | Theorem | Name |
| 4 | a,b:. a | b (c:. b = ac ) | [divides_nchar] |
| cites the following: | ||
| 3 | a,b:. ab>0 a>0 & b>0 a<0 & b<0 | [pos_mul_arg_bounds] |
| 2 | a,b:. 0<ab | [mul_bounds_1b] |