m,n,x:
. m
n 
(x+1)
m(x+1)nThm* (
m:hnum. all
Thm* (
m:hnum. (n:hnum. all
Thm* (
m:hnum. (n:hnum. (p:hnum. equal
Thm* (
m:hnum. (n:hnum. (p:hnum. (le(m,n)
Thm* (
m:hnum. (n:hnum. (p:hnum. ,le(mult(suc(p),m),mult(suc(p),n))))))| Theorem | Name |
| m,n,x:. mn (x+1)m(x+1)n | [mult_less_eq_suc] |
| 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. (le(m,n)
Thm* ( m:hnum. (n:hnum. (p:hnum. ,le(mult(suc(p),m),mult(suc(p),n)))))) | [hmult_less_eq_suc] |