m,n:
. 
m = n 
m+1
n 
n+1mThm* (
m:hnum. all
Thm* (
m:hnum. (n:hnum. equal(not(equal(m,n)),or(le(suc(m),n),le(suc(n),m)))))| Theorem | Name |
| m,n:. m = n m+1n n+1m | [not_num_eq] |
| cites the following: | |
Thm* ( m:hnum. all
Thm* ( m:hnum. (n:hnum. equal(not(equal(m,n)),or(le(suc(m),n),le(suc(n),m))))) | [hnot_num_eq] |