a,b:
. b
a 
(c:. nnsub(a;b)<c 
a<b+c)Thm* (
a:hnum. all
Thm* (
a:hnum. (b:hnum. implies
Thm* (
a:hnum. (b:hnum. (le(b,a)
Thm* (
a:hnum. (b:hnum. ,all(c:hnum. equal(lt(sub(a,b),c),lt(a,add(b,c)))))))| Theorem | Name |
| a,b:. ba (c:. nnsub(a;b)<c a<b+c) | [less_eq_sub_less] |
| cites the following: | |
Thm* ( a:hnum. all
Thm* ( a:hnum. (b:hnum. implies
Thm* ( a:hnum. (b:hnum. (le(b,a)
Thm* ( a:hnum. (b:hnum. ,all(c:hnum. equal(lt(sub(a,b),c),lt(a,add(b,c))))))) | [hless_eq_sub_less] |