m,n,x:
. m+x
n+x 
mnThm* (
m:hnum. all(n:hnum. all(p:hnum. equal(le(add(m,p),add(n,p)),le(m,n)))))| Theorem | Name |
| m,n,x:. m+xn+x mn | [less_eq_mono_add_eq] |
| cites the following: | |
Thm* ( m:hnum. all(n:hnum. all(p:hnum. equal(le(add(m,p),add(n,p)),le(m,n))))) | [hless_eq_mono_add_eq] |