c,b:
. c
b 
(a:. nnsub(a+b;c) = a+nnsub(b;c))Thm* (
c:hnum. all
Thm* (
c:hnum. (b:hnum. implies
Thm* (
c:hnum. (b:hnum. (le(c,b)
Thm* (
c:hnum. (b:hnum. ,all
Thm* (
c:hnum. (b:hnum. ,(a:hnum. equal(sub(add(a,b),c),add(a,sub(b,c)))))))| Theorem | Name |
| c,b:. cb (a:. nnsub(a+b;c) = a+nnsub(b;c)) | [less_eq_add_sub] |
| cites the following: | |
Thm* ( c:hnum. all
Thm* ( c:hnum. (b:hnum. implies
Thm* ( c:hnum. (b:hnum. (le(c,b)
Thm* ( c:hnum. (b:hnum. ,all
Thm* ( c:hnum. (b:hnum. ,(a:hnum. equal(sub(add(a,b),c),add(a,sub(b,c))))))) | [hless_eq_add_sub] |