m,n:
. 
m<n & m = n 
n<mThm* (
m:hnum. all(n:hnum. implies(and(not(lt(m,n)),not(equal(m,n))),lt(n,m))))| Theorem | Name |
| m,n:. m<n & m = n n<m | [less_cases_imp] |
| cites the following: | |
Thm* ( m:hnum. all(n:hnum. implies(and(not(lt(m,n)),not(equal(m,n))),lt(n,m)))) | [hless_cases_imp] |