m,n:
. 0<m & 0<n 
(pre(m) = pre(n) 
m = n)Thm* (
m:hnum. all
Thm* (
m:hnum. (n:hnum. implies
Thm* (
m:hnum. (n:hnum. (and(lt(0,m),lt(0,n))
Thm* (
m:hnum. (n:hnum. ,equal(equal(pre(m),pre(n)),equal(m,n)))))| Theorem | Name |
| m,n:. 0<m & 0<n (pre(m) = pre(n) m = n) | [inv_pre_eq] |
| cites the following: | |
Thm* ( m:hnum. all
Thm* ( m:hnum. (n:hnum. implies
Thm* ( m:hnum. (n:hnum. (and(lt(0,m),lt(0,n))
Thm* ( m:hnum. (n:hnum. ,equal(equal(pre(m),pre(n)),equal(m,n))))) | [hinv_pre_eq] |