m,n,x:
. m+n
m+x 
nxThm* (
m:hnum. all(n:hnum. all(p:hnum. equal(le(add(m,n),add(m,p)),le(n,p)))))| Theorem | Name |
| m,n,x:. m+nm+x nx | [add_mono_less_eq] |
| cites the following: | |
Thm* ( m:hnum. all(n:hnum. all(p:hnum. equal(le(add(m,n),add(m,p)),le(n,p))))) | [hadd_mono_less_eq] |