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.