Formal Specification of a parity test

Consider the following declarations:

Definition Even (n:nat) : Prop :=
 exists p:nat, n = 2*p. 

Definition Odd (n:nat) : Prop :=
 exists p:nat, n = S (2*p).

Inductive even_spec (n:nat) : bool -> Prop :=
| even_true : forall (Heven : Even n), even_spec n true 
| even_false : forall (Hodd : Odd n), even_spec n false.

Definition even_test_ok (f : nat -> bool) :=
 forall n:nat, even_spec n (f n).

Define a function even_bool such that even_test_ok even_bool holds.

Prove the following lemma:

Lemma even_bool_false (f: nat->bool) (H: even_test_ok f):
 forall n,  Odd n <-> f n = false.

Solution:
Prove the following lemma: Look at This file