m,i,n:
. (n+1)
m<(n+1)i 
m<iThm* (
m:hnum. all
Thm* (
m:hnum. (i:hnum. all
Thm* (
m:hnum. (i:hnum. (n:hnum. equal
Thm* (
m:hnum. (i:hnum. (n:hnum. (lt(mult(suc(n),m),mult(suc(n),i))
Thm* (
m:hnum. (i:hnum. (n:hnum. ,lt(m,i)))))| Theorem | Name |
| m,i,n:. (n+1)m<(n+1)i m<i | [less_mult_mono] |
| cites the following: | |
Thm* ( m:hnum. all
Thm* ( m:hnum. (i:hnum. all
Thm* ( m:hnum. (i:hnum. (n:hnum. equal
Thm* ( m:hnum. (i:hnum. (n:hnum. (lt(mult(suc(n),m),mult(suc(n),i))
Thm* ( m:hnum. (i:hnum. (n:hnum. ,lt(m,i))))) | [hless_mult_mono] |