This file contains theorems about the even and odd predicates on the natural numbers.
Simp attribute for lemmas about even
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.
Alias of nat.neg_one_sq.