## 練習問題:  ★★ (ev_plus4)
~~~ { .v }
Definition ev_plus4 : forall n, ev n -> ev (4 + n) :=
  fun n : nat => fun H : ev n => (ev_SS (S (S n)) (ev_SS n H)).

Theorem ev_plus4' : forall n,
  ev n -> ev (4 + n).
Proof.
  intros.
  simpl.
  apply ev_SS.                              (* Goal : ev SSSSn *)
  apply ev_SS.                              (* Goal : ev SSn *)
  apply H.                                  (* Goal : n *)
Qed.
~~~

## 練習問題:  ★★★ (ev_ev_even)
~~~ { .v }
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.  
  SearchAbout ev.
  apply SSev_even.
  apply H1.
Qed.
~~~