m,n:
. m = n 
m<n 
m<n+1
m:hnum. all(n:hnum. implies(or(equal(m,n),lt(m,n)),lt(m,suc(n)))))| Theorem | Name |
| m,n:. m = n m<n m<n+1 | [less_lemma2] |
| cites the following: | |
| m:hnum. all(n:hnum. implies(or(equal(m,n),lt(m,n)),lt(m,suc(n))))) | [hless_lemma2] |