n,m:
. n<m 
(
x:. n = x+m 
)
n:hnum. all(m:hnum. or(lt(n,m),exists(p:hnum. equal(n,add(p,m))))))| Theorem | Name |
| n,m:. n<m (x:. n = x+m ) | [less_or_eq_add] |
| cites the following: | |
| n:hnum. all(m:hnum. or(lt(n,m),exists(p:hnum. equal(n,add(p,m)))))) | [hless_or_eq_add] |