m:
. 0<m 
(n:. pre(m)<pre(n) 
m<n)Thm* (
m:hnum. implies(lt(0,m),all(n:hnum. equal(lt(pre(m),pre(n)),lt(m,n)))))| Theorem | Name |
| m:. 0<m (n:. pre(m)<pre(n) m<n) | [inv_pre_less] |
| cites the following: | |
Thm* ( m:hnum. implies(lt(0,m),all(n:hnum. equal(lt(pre(m),pre(n)),lt(m,n))))) | [hinv_pre_less] |