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