m,n:
. 0<n 
(m = pre(n) 
m+1 = n 
)Thm* (
m:hnum. all
Thm* (
m:hnum. (n:hnum. implies
Thm* (
m:hnum. (n:hnum. (lt(0,n)
Thm* (
m:hnum. (n:hnum. ,equal(equal(m,pre(n)),equal(suc(m),n)))))| Theorem | Name |
| m,n:. 0<n (m = pre(n) m+1 = n ) | [pre_suc_eq] |
| cites the following: | |
Thm* ( m:hnum. all
Thm* ( m:hnum. (n:hnum. implies
Thm* ( m:hnum. (n:hnum. (lt(0,n)
Thm* ( m:hnum. (n:hnum. ,equal(equal(m,pre(n)),equal(suc(m),n))))) | [hpre_suc_eq] |