b,a:
. b
(b -- a)+aa,b,c:. imax(a;b)+c = imax(a+c;b+c)a,b,c:. aimax(b;c) 
ab 
ac| Theorem | Name |
| b,a:. b(b -- a)+a | [ndiff_bound] |
| cites the following: | |
| a,b,c:. imax(a;b)+c = imax(a+c;b+c) | [imax_add_r] |
| a,b,c:. aimax(b;c) ab ac | [imax_ub] |