m,n:
. nnsub(m;n) = m 
m = 0 
n = 0 Thm* (
m:hnum. all(n:hnum. equal(equal(sub(m,n),m),or(equal(m,0),equal(n,0)))))| Theorem | Name |
| m,n:. nnsub(m;n) = m m = 0 n = 0 | [sub_eq_eq_0] |
| cites the following: | |
Thm* ( m:hnum. all(n:hnum. equal(equal(sub(m,n),m),or(equal(m,0),equal(n,0))))) | [hsub_eq_eq_0] |