m,n:
. odd(m
n) 
odd(m) & odd(n)
m:hnum. all(n:hnum. equal(odd(mult(m,n)),and(odd(m),odd(n)))))| Theorem | Name |
| m,n:. odd(mn) odd(m) & odd(n) | [odd_mult] |
| cites the following: | |
| m:hnum. all(n:hnum. equal(odd(mult(m,n)),and(odd(m),odd(n))))) | [hodd_mult] |