n,m:
. n<m 
(x:. n<m+x)
n:hnum. all(m:hnum. implies(lt(n,m),all(p:hnum. lt(n,add(m,p))))))| Theorem | Name |
| n,m:. n<m (x:. n<m+x) | [less_imp_less_add] |
| cites the following: | |
| n:hnum. all(m:hnum. implies(lt(n,m),all(p:hnum. lt(n,add(m,p)))))) | [hless_imp_less_add] |