Schedule/ProofCafe_23

(** 何に対して帰納法を行えばいいかを探しなさい。(ちょっとトリッキーですが) *)

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.