m,n:
. pre(nnsub(m;n)) = nnsub(pre(m);n)
m:hnum. all(n:hnum. equal(pre(sub(m,n)),sub(pre(m),n))))| Theorem | Name |
| m,n:. pre(nnsub(m;n)) = nnsub(pre(m);n) | [pre_sub] |
| cites the following: | |
| m:hnum. all(n:hnum. equal(pre(sub(m,n)),sub(pre(m),n)))) | [hpre_sub] |