proposition: Lemma even_odd_excl2: forall y:Y, ~(Y_even y /\ Y_odd y).
proof: Proof. intro. assert (Y_odd y -> ~ Y_even y). 2:tauto. pose proof (Y_odd_coind (fun x:X => ~ X_odd x) (fun y:Y => ~ Y_even y)). apply H; intuition. - destruct H1. apply H0 with y0. reflexivity. - inversion H2. apply g_inj in H3. apply H1. rewrite <- H3. assumption. - inversion H2. + apply H3 with x. reflexivity. + apply f_inj in H3. apply H1. rewrite <- H3. assumption. Qed.
imports: Coq(Classical Description) ZornsLemma(DecidableDec)