proposition: Lemma CSB_comp2: forall y:Y, CSB_bijection (CSB_bijection2 y) = y.
proof: Proof. intro. unfold CSB_bijection2; case (classic_dec (Y_even y)). - intro. unfold CSB_bijection; case (classic_dec (X_odd (g y))). + intro. destruct ginv_odd. simpl. apply g_inj. assumption. + intro. contradict n. constructor. assumption. - intro. destruct finv_noteven. simpl. unfold CSB_bijection; case (classic_dec (X_odd x)). + intro. contradict n. rewrite <- e. constructor 2. assumption. + trivial. Qed.
imports: Coq(Classical Description) ZornsLemma(DecidableDec)