m,n:
. 
n = 0 
m<m+n
m:hnum. all(n:hnum. implies(not(equal(n,0)),lt(m,add(m,n)))))| Theorem | Name |
| m,n:. n = 0 m<m+n | [less_add_nonzero] |
| cites the following: | |
| m:hnum. all(n:hnum. implies(not(equal(n,0)),lt(m,add(m,n))))) | [hless_add_nonzero] |