proposition: Lemma CSB_comp1: forall x:X, CSB_bijection2 (CSB_bijection x) = x.
proof: Proof. intro. unfold CSB_bijection; case (classic_dec (X_odd x)). - intro. destruct ginv_odd. simpl. unfold CSB_bijection2; case (classic_dec (Y_even x1)); auto. intro. destruct x0. contradict n. apply g_inj in e. rewrite e. assumption. - intro. unfold CSB_bijection2; case (classic_dec (Y_even (f x))). + intro. contradict n. inversion y. * pose proof (H x). contradict H1; reflexivity. * apply f_inj in H. rewrite <- H. assumption. + intro. destruct finv_noteven. simpl. apply f_inj. assumption. Qed.
imports: Coq(Classical Description) ZornsLemma(DecidableDec)