m,n:
. n<m 
(
x:. x+n = m 
)Thm* (
m:hnum. all
Thm* (
m:hnum. (n:hnum. implies(lt(n,m),exists(p:hnum. equal(add(p,n),m)))))| Theorem | Name |
| m,n:. n<m (x:. x+n = m ) | [less_add] |
| cites the following: | |
Thm* ( m:hnum. all
Thm* ( m:hnum. (n:hnum. implies(lt(n,m),exists(p:hnum. equal(add(p,n),m))))) | [hless_add] |