coq - 含意仮説内の式をcoqで単純化する方法

Question

次の補題を証明しようとしています。

Inductive even : nat → Prop :=
| ev_0 : even 0
| ev_SS (n : nat) (H : even n) : even (S (S n)).

Lemma even_Sn_not_even_n : forall n,
    even (S n) <-> not (even n).
Proof.
  intros n. split.
  + intros H. unfold not. intros H1. induction H1 as [|n' E' IHn].
    - inversion H.
    - inversion_clear H. apply IHn in H0. apply H0.
  + unfold not. intros H. induction n as [|n' E' IHn].
    -
Qed.

最後に得たものは次のとおりです。

1 subgoal (ID 173)

H : even 0 -> False
============================
even 1

coq で "even 0" を true に、"even 1" を false に評価するようにします。を試しましsimplたapply ev_0 in H.が、エラーが発生します。何をすべきか？