m,x:
. m
x 
(n:. nnsub(x;m)n 
xm+n)Thm* (
m:hnum. all
Thm* (
m:hnum. (p:hnum. implies
Thm* (
m:hnum. (p:hnum. (le(m,p)
Thm* (
m:hnum. (p:hnum. ,all(n:hnum. equal(le(sub(p,m),n),le(p,add(m,n)))))))| Theorem | Name |
| m,x:. mx (n:. nnsub(x;m)n xm+n) | [sub_less_eq_add] |
| cites the following: | |
Thm* ( m:hnum. all
Thm* ( m:hnum. (p:hnum. implies
Thm* ( m:hnum. (p:hnum. (le(m,p)
Thm* ( m:hnum. (p:hnum. ,all(n:hnum. equal(le(sub(p,m),n),le(p,add(m,n))))))) | [hsub_less_eq_add] |