n,m:
. exp(m+1+1;n)<exp(m+1+1;n+1)
n:hnum. all(m:hnum. lt(exp(suc(suc(m)),n),exp(suc(suc(m)),suc(n)))))| Theorem | Name |
| n,m:. exp(m+1+1;n)<exp(m+1+1;n+1) | [less_exp_suc_mono] |
| cites the following: | |
| n:hnum. all(m:hnum. lt(exp(suc(suc(m)),n),exp(suc(suc(m)),suc(n))))) | [hless_exp_suc_mono] |