m,n,x:
. (m+n)
x = mx+nx 
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(add(m,n),p)
Thm* (
m:hnum. (n:hnum. (p:hnum. ,add(mult(m,p),mult(n,p))))))| Theorem | Name |
| m,n,x:. (m+n)x = mx+nx | [right_add_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(add(m,n),p)
Thm* ( m:hnum. (n:hnum. (p:hnum. ,add(mult(m,p),mult(n,p)))))) | [hright_add_distrib] |