m,n,x:
. x<nnsub(m;n) 
n+x<mThm* (
m:hnum. all(n:hnum. all(p:hnum. equal(gt(sub(m,n),p),gt(m,add(n,p))))))| Theorem | Name |
| m,n,x:. x<nnsub(m;n) n+x<m | [sub_right_greater] |
| cites the following: | |
Thm* ( m:hnum. all(n:hnum. all(p:hnum. equal(gt(sub(m,n),p),gt(m,add(n,p)))))) | [hsub_right_greater] |