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