m,n,x:
. m<n 
m+x<n+xThm* (
m:hnum. all
Thm* (
m:hnum. (n:hnum. all(p:hnum. implies(lt(m,n),lt(add(m,p),add(n,p))))))| Theorem | Name |
| m,n,x:. m<n m+x<n+x | [less_mono_add] |
| cites the following: | |
Thm* ( m:hnum. all
Thm* ( m:hnum. (n:hnum. all(p:hnum. implies(lt(m,n),lt(add(m,p),add(n,p)))))) | [hless_mono_add] |