m,n,x:
. nnsub(nnsub(m;n);x) = nnsub(m;n+x)Thm* (
m:hnum. all
Thm* (
m:hnum. (n:hnum. all(p:hnum. equal(sub(sub(m,n),p),sub(m,add(n,p))))))| Theorem | Name |
| m,n,x:. nnsub(nnsub(m;n);x) = nnsub(m;n+x) | [sub_right_sub] |
| cites the following: | |
Thm* ( m:hnum. all
Thm* ( m:hnum. (n:hnum. all(p:hnum. equal(sub(sub(m,n),p),sub(m,add(n,p)))))) | [hsub_right_sub] |