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