n:
. odd(n) 
(
m:. n = 2
m+1 
)
n:hnum. equal(odd(n),exists(m:hnum. equal(n,suc(mult(2,m))))))| Theorem | Name |
| n:. odd(n) (m:. n = 2m+1 ) | [odd_exists] |
| cites the following: | |
| n:hnum. equal(odd(n),exists(m:hnum. equal(n,suc(mult(2,m)))))) | [hodd_exists] |