m,n,x:
. m+x<n+x 
m<nThm* (
m:hnum. all(n:hnum. all(p:hnum. equal(lt(add(m,p),add(n,p)),lt(m,n)))))| Theorem | Name |
| m,n,x:. m+x<n+x m<n | [less_mono_add_eq] |
| cites the following: | |
Thm* ( m:hnum. all(n:hnum. all(p:hnum. equal(lt(add(m,p),add(n,p)),lt(m,n))))) | [hless_mono_add_eq] |