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