a,b,c:
. nnsub(a;b+c) = nnsub(nnsub(a;b);c)Thm* (
a:hnum. all
Thm* (
a:hnum. (b:hnum. all(c:hnum. equal(sub(a,add(b,c)),sub(sub(a,b),c)))))| Theorem | Name |
| a,b,c:. nnsub(a;b+c) = nnsub(nnsub(a;b);c) | [sub_plus] |
| cites the following: | |
Thm* ( a:hnum. all
Thm* ( a:hnum. (b:hnum. all(c:hnum. equal(sub(a,add(b,c)),sub(sub(a,b),c))))) | [hsub_plus] |