(** 何に対して帰納法を行えばいいかを探しなさい。(ちょっとトリッキーですが) *)
Theorem ev_ev_even : forall n m,
  ev (n+m) -> ev n -> ev m.
Proof.
  intros n m H1 H2.
  induction H2.
  apply H1.

  apply IHev.
  simpl in H1.  
  cut (forall l, ev (S (S l)) -> ev l).
  intros.
  apply H.
  apply H1.

  intros.
  inversion H.
  apply H3.
Qed.