m,n,x:
. m
nnsub(n;x) 
m+xn 
m0Thm* (
m:hnum. all
Thm* (
m:hnum. (n:hnum. all
Thm* (
m:hnum. (n:hnum. (p:hnum. equal
Thm* (
m:hnum. (n:hnum. (p:hnum. (le(m,sub(n,p))
Thm* (
m:hnum. (n:hnum. (p:hnum. ,or(le(add(m,p),n),le(m,0))))))| Theorem | Name |
| m,n,x:. mnnsub(n;x) m+xn m0 | [sub_left_less_eq] |
| cites the following: | |
Thm* ( m:hnum. all
Thm* ( m:hnum. (n:hnum. all
Thm* ( m:hnum. (n:hnum. (p:hnum. equal
Thm* ( m:hnum. (n:hnum. (p:hnum. (le(m,sub(n,p))
Thm* ( m:hnum. (n:hnum. (p:hnum. ,or(le(add(m,p),n),le(m,0)))))) | [hsub_left_less_eq] |