Inductive even : nat -> Prop :=
| ev_0 : even 0
| ev_2 : even 2
| ev_sum : forall n m, even n -> even m -> even (n + m).

Inductive ev : nat -> Prop :=
| e_0 : ev 0
| e_SS : forall n, ev n -> ev (S (S n)).

Lemma induction_2 : forall P:nat->Prop,
  P 0 ->
  P 1 ->
  (forall n, P n -> P (S (S n))) ->
  forall n, P n.
Proof.
  intros P P_0 P_1 P_SS n.
  refine ((fix F (n:nat) := match n as n0 return P n0 with
    | O => _
    | S O => _
    | S (S n') => _
    end) n).
  - assumption.
  - assumption.
  - apply P_SS.
    apply F.
Qed.

Require Import Omega.

Theorem even_plus : forall n m, ev n -> ev m -> ev (n + m).
Proof.
  apply (induction_2 (fun n => forall m : nat, ev n -> ev m -> ev (n + m))).
  - trivial.
  - intros.
    inversion H.
  - intros.
    inversion H0.
    assert (K : S (S n) + m = n + (S (S m))).
    { omega. }
    rewrite K.
    apply H.
    + assumption.
    + constructor. assumption.
Qed.

Theorem ev_implies_even : forall n, ev n -> even n.
Proof.
  apply (induction_2 (fun n => ev n -> even n )).
  - constructor.
  - intros H. inversion H.
  - intros n IHn H.
    inversion H.
    apply (ev_sum 2 n).
    + exact ev_2.
    + apply IHn. assumption.
Qed.

Theorem even_implies_ev : forall n, even n -> ev n.
Proof.
  intros n H.
  induction H.
  - constructor.
  - exact (e_SS 0 e_0).
  - apply even_plus.
    + assumption.
    + assumption.
Qed.

Theorem even_eq_ev : forall n, even n <-> ev n.
Proof.
  split.
  - apply even_implies_ev.
  - apply ev_implies_even.
Qed.