m,n:
. odd(m+n) 
(odd(m) odd(n))
m:hnum. all(n:hnum. equal(odd(add(m,n)),not(equal(odd(m),odd(n))))))| Theorem | Name |
| m,n:. odd(m+n) (odd(m) odd(n)) | [odd_add] |
| cites the following: | |
| m:hnum. all(n:hnum. equal(odd(add(m,n)),not(equal(odd(m),odd(n)))))) | [hodd_add] |