m,n:
. even(m
n) 
even(m) 
even(n)
m:hnum. all(n:hnum. equal(even(mult(m,n)),or(even(m),even(n)))))| Theorem | Name |
| m,n:. even(mn) even(m) even(n) | [even_mult] |
| cites the following: | |
| m:hnum. all(n:hnum. equal(even(mult(m,n)),or(even(m),even(n))))) | [heven_mult] |