m,n:
. m<n & 
n = m+1 
m+1<nThm* (
m:hnum. all
Thm* (
m:hnum. (n:hnum. implies
Thm* (
m:hnum. (n:hnum. (and(lt(m,n),not(equal(n,suc(m))))
Thm* (
m:hnum. (n:hnum. ,lt(suc(m),n))))| Theorem | Name |
| m,n:. m<n & n = m+1 m+1<n | [less_not_suc] |
| cites the following: | |
Thm* ( m:hnum. all
Thm* ( m:hnum. (n:hnum. implies
Thm* ( m:hnum. (n:hnum. (and(lt(m,n),not(equal(n,suc(m))))
Thm* ( m:hnum. (n:hnum. ,lt(suc(m),n)))) | [hless_not_suc] |