m,n,x:
. nnsub(n;x)
m 
nm+xThm* (
m:hnum. all(n:hnum. all(p:hnum. equal(ge(m,sub(n,p)),ge(add(m,p),n)))))| Theorem | Name |
| m,n,x:. nnsub(n;x)m nm+x | [sub_left_greater_eq] |
| cites the following: | |
Thm* ( m:hnum. all(n:hnum. all(p:hnum. equal(ge(m,sub(n,p)),ge(add(m,p),n))))) | [hsub_left_greater_eq] |