m,n,x:
. x
nnsub(m;n) = nnsub(xm;xn)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. (mult(p,sub(m,n))
Thm* (
m:hnum. (n:hnum. (p:hnum. ,sub(mult(p,m),mult(p,n))))))| Theorem | Name |
| m,n,x:. xnnsub(m;n) = nnsub(xm;xn) | [left_sub_distrib] |
| 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. (mult(p,sub(m,n))
Thm* ( m:hnum. (n:hnum. (p:hnum. ,sub(mult(p,m),mult(p,n)))))) | [hleft_sub_distrib] |