This file contains theorems about the Even and Odd predicates on the natural numbers.
If m and n are natural numbers, then the natural number m^n is even
if and only if m is even and n is positive.
If a is even, then n is odd iff n % a is odd.
n % a
If a is even, then n is even iff n % a is even.
If n is odd and a is even, then n % a is odd.
If n is even and a is even, then n % a is even.
2 is not a factor of an odd natural number.