m,n:
. m
n 
(
x:. n = m+x 
)Thm* (
m:hnum. all
Thm* (
m:hnum. (n:hnum. implies(le(m,n),exists(p:hnum. equal(n,add(m,p))))))| Theorem | Name |
| m,n:. mn (x:. n = m+x ) | [less_equal_add] |
| cites the following: | |
Thm* ( m:hnum. all
Thm* ( m:hnum. (n:hnum. implies(le(m,n),exists(p:hnum. equal(n,add(m,p)))))) | [hless_equal_add] |