m,n,x:
. m<nnsub(n;x) 
m+x<nThm* (
m:hnum. all(n:hnum. all(p:hnum. equal(lt(m,sub(n,p)),lt(add(m,p),n)))))| Theorem | Name |
| m,n,x:. m<nnsub(n;x) m+x<n | [sub_left_less] |
| cites the following: | |
Thm* ( m:hnum. all(n:hnum. all(p:hnum. equal(lt(m,sub(n,p)),lt(add(m,p),n))))) | [hsub_left_less] |