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.
cut (forall l, ev (S (S l)) -> ev l). intros. apply H. apply H1.

intros. inversion H. apply H3. Qed.