m,n:
. n
m 
nnsub(m;n)+n = m 
m:hnum. all(n:hnum. implies(le(n,m),equal(add(sub(m,n),n),m))))| Theorem | Name |
| m,n:. nm nnsub(m;n)+n = m | [sub_add] |
| cites the following: | |
| m:hnum. all(n:hnum. implies(le(n,m),equal(add(sub(m,n),n),m)))) | [hsub_add] |