n,m,i:
. i<nnsub(n;m) 
i+m<nThm* (
n:hnum. all
Thm* (
n:hnum. (m:hnum. all(i:hnum. implies(lt(i,sub(n,m)),lt(add(i,m),n)))))| Theorem | Name |
| n,m,i:. i<nnsub(n;m) i+m<n | [less_sub_add_less] |
| cites the following: | |
Thm* ( n:hnum. all
Thm* ( n:hnum. (m:hnum. all(i:hnum. implies(lt(i,sub(n,m)),lt(add(i,m),n))))) | [hless_sub_add_less] |