Nota : this file is OBSOLETE, and left only for compatibility.
Please consider instead predicates
Nat.Even and
Nat.Odd
and Boolean functions
Nat.even and
Nat.odd.
Here we define the predicates
even and
odd by mutual induction
and we prove the decidability and the exclusion of those predicates.
The main results about parity are proved in the module Div2.