m,n,x:
. x
nnsub(m;n) 
n+xm 
x0Thm* (
m:hnum. all
Thm* (
m:hnum. (n:hnum. all
Thm* (
m:hnum. (n:hnum. (p:hnum. equal
Thm* (
m:hnum. (n:hnum. (p:hnum. (ge(sub(m,n),p)
Thm* (
m:hnum. (n:hnum. (p:hnum. ,or(ge(m,add(n,p)),ge(0,p))))))| Theorem | Name |
| m,n,x:. xnnsub(m;n) n+xm x0 | [sub_right_greater_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. (ge(sub(m,n),p)
Thm* ( m:hnum. (n:hnum. (p:hnum. ,or(ge(m,add(n,p)),ge(0,p)))))) | [hsub_right_greater_eq] |